Mathlib v3 is deprecated. Go to Mathlib v4

Def witt_vector.witt_mul_n

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.witt_mul_nView on Github →