feat(FieldTheory/Minpoly): remove IsIntegral condition for lemmas (#…

…17080) Remove `IsIntegral` condition for `minpoly.add_algebraMap` and `minpoly.sub_algebraMap`.
leanprover-community · Sep 25, 2024 · 88787b2 · 88787b2
1 parent 691fdda
commit 88787b2
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 15 deletions.
diff --git a/Mathlib/FieldTheory/Minpoly/Field.lean b/Mathlib/FieldTheory/Minpoly/Field.lean
@@ -127,22 +127,26 @@ theorem eq_of_irreducible [Nontrivial B] {p : A[X]} (hp1 : Irreducible p)
   · rw [aeval_mul, hp2, zero_mul]
   · rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel₀]
 
-theorem add_algebraMap {B : Type*} [CommRing B] [Algebra A B] {x : B} (hx : IsIntegral A x)
+theorem add_algebraMap {B : Type*} [CommRing B] [Algebra A B] (x : B)
     (a : A) : minpoly A (x + algebraMap A B a) = (minpoly A x).comp (X - C a) := by
-  refine (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) ?_ fun q qmo hq => ?_).symm
-  · simp [aeval_comp]
-  · have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq
-    have H := minpoly.min A x (qmo.comp_X_add_C _) this
-    rw [degree_eq_natDegree qmo.ne_zero,
-      degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero, natDegree_comp,
-      natDegree_X_sub_C, mul_one]
-    rwa [degree_eq_natDegree (minpoly.ne_zero hx),
-      degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
-      natDegree_X_add_C, mul_one] at H
-
-theorem sub_algebraMap {B : Type*} [CommRing B] [Algebra A B] {x : B} (hx : IsIntegral A x)
+  by_cases hx : IsIntegral A x
+  · refine (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) ?_ fun q qmo hq => ?_).symm
+    · simp [aeval_comp]
+    · have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq
+      have H := minpoly.min A x (qmo.comp_X_add_C _) this
+      rw [degree_eq_natDegree qmo.ne_zero,
+        degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero, natDegree_comp,
+        natDegree_X_sub_C, mul_one]
+      rwa [degree_eq_natDegree (minpoly.ne_zero hx),
+        degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
+        natDegree_X_add_C, mul_one] at H
+  · rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]
+    refine fun h ↦ hx ?_
+    simpa only [add_sub_cancel_right] using IsIntegral.sub h (isIntegral_algebraMap (x := a))
+
+theorem sub_algebraMap {B : Type*} [CommRing B] [Algebra A B] {x : B}
     (a : A) : minpoly A (x - algebraMap A B a) = (minpoly A x).comp (X + C a) := by
-  simpa [sub_eq_add_neg] using add_algebraMap hx (-a)
+  simpa [sub_eq_add_neg] using add_algebraMap x (-a)
 
 section AlgHomFintype
 

diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
@@ -379,7 +379,7 @@ theorem minpoly_sub_one_eq_cyclotomic_comp [Algebra K A] [IsDomain A] {ζ : A}
     minpoly K (ζ - 1) = (cyclotomic n K).comp (X + 1) := by
   haveI := IsCyclotomicExtension.neZero' n K A
   rw [show ζ - 1 = ζ + algebraMap K A (-1) by simp [sub_eq_add_neg],
-    minpoly.add_algebraMap ((integral {n} K A).isIntegral ζ),
+    minpoly.add_algebraMap ζ,
     hζ.minpoly_eq_cyclotomic_of_irreducible h]
   simp