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

leanprover-community · Jun 5, 2023 · bcdc81c · bcdc81c
1 parent 041a489
commit bcdc81c
Show file tree

Hide file tree

Showing 3 changed files with 425 additions and 7 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2296,6 +2296,7 @@ import Mathlib.RingTheory.Valuation.ExtendToLocalization
 import Mathlib.RingTheory.Valuation.Integers
 import Mathlib.RingTheory.Valuation.Integral
 import Mathlib.RingTheory.Valuation.Quotient
+import Mathlib.RingTheory.WittVector.StructurePolynomial
 import Mathlib.RingTheory.WittVector.WittPolynomial
 import Mathlib.RingTheory.ZMod
 import Mathlib.SetTheory.Cardinal.Basic

diff --git a/Mathlib/FieldTheory/Finite/Polynomial.lean b/Mathlib/FieldTheory/Finite/Polynomial.lean
@@ -25,27 +25,27 @@ variable {σ : Type _}
 
 /-- A polynomial over the integers is divisible by `n : ℕ`
 if and only if it is zero over `ZMod n`. -/
-theorem c_dvd_iff_zMod (n : ℕ) (φ : MvPolynomial σ ℤ) :
+theorem C_dvd_iff_zmod (n : ℕ) (φ : MvPolynomial σ ℤ) :
     C (n : ℤ) ∣ φ ↔ map (Int.castRingHom (ZMod n)) φ = 0 :=
   C_dvd_iff_map_hom_eq_zero _ _ (CharP.int_cast_eq_zero_iff (ZMod n) n) _
 set_option linter.uppercaseLean3 false in
-#align mv_polynomial.C_dvd_iff_zmod MvPolynomial.c_dvd_iff_zMod
+#align mv_polynomial.C_dvd_iff_zmod MvPolynomial.C_dvd_iff_zmod
 
 section frobenius
 
 variable {p : ℕ} [Fact p.Prime]
 
-theorem frobenius_zMod (f : MvPolynomial σ (ZMod p)) : frobenius _ p f = expand p f := by
+theorem frobenius_zmod (f : MvPolynomial σ (ZMod p)) : frobenius _ p f = expand p f := by
   apply induction_on f
   · intro a; rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]
   · simp only [AlgHom.map_add, RingHom.map_add]; intro _ _ hf hg; rw [hf, hg]
   · simp only [expand_X, RingHom.map_mul, AlgHom.map_mul]
     intro _ _ hf; rw [hf, frobenius_def]
-#align mv_polynomial.frobenius_zmod MvPolynomial.frobenius_zMod
+#align mv_polynomial.frobenius_zmod MvPolynomial.frobenius_zmod
 
-theorem expand_zMod (f : MvPolynomial σ (ZMod p)) : expand p f = f ^ p :=
-  (frobenius_zMod _).symm
-#align mv_polynomial.expand_zmod MvPolynomial.expand_zMod
+theorem expand_zmod (f : MvPolynomial σ (ZMod p)) : expand p f = f ^ p :=
+  (frobenius_zmod _).symm
+#align mv_polynomial.expand_zmod MvPolynomial.expand_zmod
 
 end frobenius