Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-19 22:45 b707e989

View on Github →

refactor(ring_theory/witt_vector): move lemmas to separate file (#4693) This new file has almost no module docstring. This is on purpose, it is a refactor PR. A follow-up PR will add a module docstring and more definitions. Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes