Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-23 10:15 04b55727

View on Github →

feat(ring_theory/witt_vector/defs): type of witt vectors + ring operations (#4332) Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes

added theorem witt_vector.add_coeff
added theorem witt_vector.coeff_mk
added def witt_vector.eval
added theorem witt_vector.ext
added theorem witt_vector.ext_iff
added def witt_vector.mk
added theorem witt_vector.mul_coeff
added theorem witt_vector.neg_coeff
added theorem witt_vector.zero_coeff
added def witt_vector