Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-27 18:30 73a2fd3a

View on Github →

feat(ring_theory/witt_vector/init_tail): adding disjoint witt vectors (#4835) Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes

Created src/ring_theory/witt_vector/init_tail.lean

added theorem witt_vector.coeff_add_of_disjoint

added theorem witt_vector.coeff_select

added def witt_vector.init

added theorem witt_vector.init_add

added theorem witt_vector.init_add_tail

added theorem witt_vector.init_init

added theorem witt_vector.init_is_poly

added theorem witt_vector.init_mul

added theorem witt_vector.init_neg

added theorem witt_vector.init_sub

added def witt_vector.select

added theorem witt_vector.select_add_select_not

added theorem witt_vector.select_is_poly

added def witt_vector.select_poly

added def witt_vector.tail