Commit 2023-06-27 14:42 c2df547e

View on Github →

feat: port RingTheory.WittVector.Frobenius (#4887)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/Frobenius.lean

added theorem WittVector.bind₁_frobeniusPolyRat_wittPolynomial

added theorem WittVector.bind₁_frobeniusPoly_wittPolynomial

added theorem WittVector.coeff_frobenius

added theorem WittVector.coeff_frobeniusFun

added theorem WittVector.coeff_frobenius_charP

added def WittVector.frobenius

added def WittVector.frobeniusEquiv

added def WittVector.frobeniusFun

added def WittVector.frobeniusPoly

added theorem WittVector.frobeniusPolyAux_eq

added def WittVector.frobeniusPolyRat

added theorem WittVector.frobeniusPoly_zMod

added theorem WittVector.frobenius_bijective

added theorem WittVector.frobenius_eq_map_frobenius

added theorem WittVector.frobenius_zmodp

added theorem WittVector.ghostComponent_frobenius

added theorem WittVector.ghostComponent_frobeniusFun

added theorem WittVector.map_frobeniusPoly.key₁

added theorem WittVector.map_frobeniusPoly.key₂

added theorem WittVector.map_frobeniusPoly