Mathlib v3 is deprecated. Go to Mathlib v4

Theorem witt_vector.mul_n_is_poly

Modification history

2020-11-10 10:21
src/ring_theory/witt_vector/mul_p.lean
feat(ring_theory/witt_vector/mul_p): multiplication by p as operation on witt vectors (#4837) …
Added witt_vector.mul_n_is_polyView on Github →