Commit 2023-06-05 05:13 bcdc81c0

View on Github →

feat: port RingTheory.WittVector.StructurePolynomial (#4633)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/Finite/Polynomial.lean

added theorem MvPolynomial.C_dvd_iff_zmod

deleted theorem MvPolynomial.c_dvd_iff_zMod

deleted theorem MvPolynomial.expand_zMod

added theorem MvPolynomial.expand_zmod

deleted theorem MvPolynomial.frobenius_zMod

added theorem MvPolynomial.frobenius_zmod

Created Mathlib/RingTheory/WittVector/StructurePolynomial.lean

added theorem C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum

added theorem bind₁_rename_expand_wittPolynomial

added theorem constantCoeff_wittStructureInt

added theorem constantCoeff_wittStructureInt_zero

added theorem constantCoeff_wittStructureRat

added theorem constantCoeff_wittStructureRat_zero

added theorem eq_wittStructureInt

added theorem map_wittStructureInt

added theorem wittStructureInt_existsUnique

added theorem wittStructureInt_prop

added theorem wittStructureInt_rename

added theorem wittStructureInt_vars

added theorem wittStructureRat_existsUnique

added theorem wittStructureRat_prop

added theorem wittStructureRat_rec

added theorem wittStructureRat_rec_aux

added theorem wittStructureRat_vars

added theorem witt_structure_prop