Mathlib v3 is deprecated. Go to Mathlib v4

Theorem witt_vector.map_frobenius_poly.key₂

Modification history

2023-02-27 10:42
src/ring_theory/witt_vector/frobenius.lean
feat(data/nat/multiplicity): rename `nat.multiplicity_choose_prime_pow`, add lemmas (#18183) …
Modified witt_vector.map_frobenius_poly.key₂View on Github →
2020-12-03 14:04
src/ring_theory/witt_vector/frobenius.lean
feat(ring_theory/witt_vector/frobenius): the frobenius endomorphism of witt vectors (#4838) …
Added witt_vector.map_frobenius_poly.key₂View on Github →