Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-03 14:04 e7c2bba1

View on Github →

feat(ring_theory/witt_vector/frobenius): the frobenius endomorphism of witt vectors (#4838) Co-Authored-By: Rob Y. Lewis [email protected]

Estimated changes

Created src/ring_theory/witt_vector/frobenius.lean

added theorem witt_vector.bind₁_frobenius_poly_rat_witt_polynomial

added theorem witt_vector.bind₁_frobenius_poly_witt_polynomial

added theorem witt_vector.coeff_frobenius

added theorem witt_vector.coeff_frobenius_char_p

added theorem witt_vector.coeff_frobenius_fun

added def witt_vector.frobenius

added theorem witt_vector.frobenius_eq_map_frobenius

added def witt_vector.frobenius_fun

added theorem witt_vector.frobenius_fun_is_poly

added theorem witt_vector.frobenius_is_poly

added def witt_vector.frobenius_poly

added theorem witt_vector.frobenius_poly_aux_eq

added def witt_vector.frobenius_poly_rat

added theorem witt_vector.frobenius_poly_zmod

added theorem witt_vector.frobenius_zmodp

added theorem witt_vector.ghost_component_frobenius

added theorem witt_vector.ghost_component_frobenius_fun

added theorem witt_vector.map_frobenius_poly.key₁

added theorem witt_vector.map_frobenius_poly.key₂

added theorem witt_vector.map_frobenius_poly