Mathlib v3 is deprecated. Go to Mathlib v4

Theorem witt_vector.bind₁_witt_mul_n_witt_polynomial

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.bind₁_witt_mul_n_witt_polynomial View on Github →