From 88787b217c3255058d0046f800a349f773ce27b2 Mon Sep 17 00:00:00 2001
From: Jiang Jiedong <emailboxofjjd@163.com>
Date: Wed, 25 Sep 2024 21:17:42 +0000
Subject: [PATCH] feat(FieldTheory/Minpoly): remove `IsIntegral` condition for
 lemmas (#17080)

Remove `IsIntegral` condition for `minpoly.add_algebraMap` and `minpoly.sub_algebraMap`.
---
 Mathlib/FieldTheory/Minpoly/Field.lean        | 32 +++++++++++--------
 .../Cyclotomic/PrimitiveRoots.lean            |  2 +-
 2 files changed, 19 insertions(+), 15 deletions(-)

diff --git a/Mathlib/FieldTheory/Minpoly/Field.lean b/Mathlib/FieldTheory/Minpoly/Field.lean
index 32d3a549998d0..b62efc1339b8a 100644
--- 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
index e8b1549b25e66..33bb6cad832cd 100644
--- 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