chore: replace minpoly.eq_of_algebraMap_eq by algebraMap_eq (#7228)

Also changes the repetitive names `minpoly.minpoly_algHom/Equiv` to `minpoly.algHom/Equiv_eq`

Author: alreadydone

Mathlib/FieldTheory/AbelRuffini.lean

@@ -394,7 +394,7 @@ theorem isSolvable' {α : E} {q : F[X]} (q_irred : Irreducible q) (q_aeval : aev
   have : _root_.IsSolvable (q * C q.leadingCoeff⁻¹).Gal := by
     rw [minpoly.eq_of_irreducible q_irred q_aeval, ←
       show minpoly F (⟨α, hα⟩ : solvableByRad F E) = minpoly F α from
-        minpoly.eq_of_algebraMap_eq (RingHom.injective _) (isIntegral ⟨α, hα⟩) rfl]
+        (minpoly.algebraMap_eq (RingHom.injective _) _).symm]
     exact isSolvable ⟨α, hα⟩
   refine' solvable_of_surjective (Gal.restrictDvd_surjective ⟨C q.leadingCoeff⁻¹, rfl⟩ _)
   rw [mul_ne_zero_iff, Ne, Ne, C_eq_zero, inv_eq_zero]

Mathlib/FieldTheory/Adjoin.lean

@@ -795,20 +795,14 @@ end AdjoinIntermediateFieldLattice
 
 section AdjoinIntegralElement
 
-variable {F : Type*} [Field F] {E : Type*} [Field E] [Algebra F E] {α : E}
+variable (F : Type*) [Field F] {E : Type*} [Field E] [Algebra F E] {α : E}
 
 variable {K : Type*} [Field K] [Algebra F K]
 
-theorem minpoly_gen {α : E} (h : IsIntegral F α) :
+theorem minpoly_gen (α : E) :
     minpoly F (AdjoinSimple.gen F α) = minpoly F α := by
-  rw [← AdjoinSimple.algebraMap_gen F α] at h
-  have inj := (algebraMap F⟮α⟯ E).injective
-  exact
-    minpoly.eq_of_algebraMap_eq inj ((isIntegral_algebraMap_iff inj).mp h)
-      (AdjoinSimple.algebraMap_gen _ _).symm
-#align intermediate_field.minpoly_gen IntermediateField.minpoly_gen
-
-variable (F)
+  rw [← minpoly.algebraMap_eq (algebraMap F⟮α⟯ E).injective, AdjoinSimple.algebraMap_gen]
+#align intermediate_field.minpoly_gen IntermediateField.minpoly_genₓ
 
 theorem aeval_gen_minpoly (α : E) : aeval (AdjoinSimple.gen F α) (minpoly F α) = 0 := by
   ext
@@ -899,7 +893,7 @@ noncomputable def algHomAdjoinIntegralEquiv (h : IsIntegral F α) :
     (F⟮α⟯ →ₐ[F] K) ≃ { x // x ∈ (minpoly F α).aroots K } :=
   (adjoin.powerBasis h).liftEquiv'.trans
     ((Equiv.refl _).subtypeEquiv fun x => by
-      rw [adjoin.powerBasis_gen, minpoly_gen h, Equiv.refl_apply])
+      rw [adjoin.powerBasis_gen, minpoly_gen, Equiv.refl_apply])
 #align intermediate_field.alg_hom_adjoin_integral_equiv IntermediateField.algHomAdjoinIntegralEquiv
 
 /-- Fintype of algebra homomorphism `F⟮α⟯ →ₐ[F] K` -/
@@ -911,7 +905,7 @@ theorem card_algHom_adjoin_integral (h : IsIntegral F α) (h_sep : (minpoly F α
     (h_splits : (minpoly F α).Splits (algebraMap F K)) :
     @Fintype.card (F⟮α⟯ →ₐ[F] K) (fintypeOfAlgHomAdjoinIntegral F h) = (minpoly F α).natDegree := by
   rw [AlgHom.card_of_powerBasis] <;>
-    simp only [adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen h, h_sep, h_splits]
+    simp only [adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen, h_sep, h_splits]
 #align intermediate_field.card_alg_hom_adjoin_integral IntermediateField.card_algHom_adjoin_integral
 
 end AdjoinIntegralElement
@@ -1067,7 +1061,6 @@ noncomputable def Lifts.upperBoundAlgHom {c : Set (Lifts F E K)} (hc : IsChain (
     simp only [Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring,
       coe_toSubalgebra, Lifts.eq_of_le hzw, Lifts.eq_of_le hxw, Lifts.eq_of_le hyw, ← w.2.map_mul,
         Submonoid.mk_mul_mk]
-
   commutes' _ := AlgHom.commutes _ _
 #align intermediate_field.lifts.upper_bound_alg_hom IntermediateField.Lifts.upperBoundAlgHom
 
@@ -1281,10 +1274,8 @@ open IntermediateField
 
 /-- `pb.equivAdjoinSimple` is the equivalence between `K⟮pb.gen⟯` and `L` itself. -/
 noncomputable def equivAdjoinSimple (pb : PowerBasis K L) : K⟮pb.gen⟯ ≃ₐ[K] L :=
-  (adjoin.powerBasis pb.isIntegral_gen).equivOfMinpoly pb
-    (minpoly.eq_of_algebraMap_eq (algebraMap K⟮pb.gen⟯ L).injective
-      (adjoin.powerBasis pb.isIntegral_gen).isIntegral_gen
-      (by rw [adjoin.powerBasis_gen, AdjoinSimple.algebraMap_gen]))
+  (adjoin.powerBasis pb.isIntegral_gen).equivOfMinpoly pb <| by
+    rw [adjoin.powerBasis_gen, minpoly_gen]
 #align power_basis.equiv_adjoin_simple PowerBasis.equivAdjoinSimple
 
 @[simp]

Mathlib/FieldTheory/IntermediateField.lean

@@ -721,10 +721,8 @@ theorem isIntegral_iff {x : S} : IsIntegral K x ↔ IsIntegral K (x : L) := by
   rw [← isAlgebraic_iff_isIntegral, isAlgebraic_iff, isAlgebraic_iff_isIntegral]
 #align intermediate_field.is_integral_iff IntermediateField.isIntegral_iff
 
-theorem minpoly_eq (x : S) : minpoly K x = minpoly K (x : L) := by
-  by_cases hx : IsIntegral K x
-  · exact minpoly.eq_of_algebraMap_eq (algebraMap S L).injective hx rfl
-  · exact (minpoly.eq_zero hx).trans (minpoly.eq_zero (mt isIntegral_iff.mpr hx)).symm
+theorem minpoly_eq (x : S) : minpoly K x = minpoly K (x : L) :=
+  (minpoly.algebraMap_eq (algebraMap S L).injective x).symm
 #align intermediate_field.minpoly_eq IntermediateField.minpoly_eq
 
 end IntermediateField

Mathlib/FieldTheory/Minpoly/Basic.lean

@@ -64,16 +64,21 @@ theorem eq_zero (hx : ¬IsIntegral A x) : minpoly A x = 0 :=
   dif_neg hx
 #align minpoly.eq_zero minpoly.eq_zero
 
-theorem minpoly_algHom (f : B →ₐ[A] B') (hf : Function.Injective f) (x : B) :
+theorem algHom_eq (f : B →ₐ[A] B') (hf : Function.Injective f) (x : B) :
     minpoly A (f x) = minpoly A x := by
   refine' dif_ctx_congr (isIntegral_algHom_iff _ hf) (fun _ => _) fun _ => rfl
   simp_rw [← Polynomial.aeval_def, aeval_algHom, AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
-#align minpoly.minpoly_alg_hom minpoly.minpoly_algHom
+#align minpoly.minpoly_alg_hom minpoly.algHom_eq
+
+theorem algebraMap_eq {B} [CommRing B] [Algebra A B] [Algebra B B'] [IsScalarTower A B B']
+    (h : Function.Injective (algebraMap B B')) (x : B) :
+    minpoly A (algebraMap B B' x) = minpoly A x :=
+  algHom_eq (IsScalarTower.toAlgHom A B B') h x
 
 @[simp]
-theorem minpoly_algEquiv (f : B ≃ₐ[A] B') (x : B) : minpoly A (f x) = minpoly A x :=
-  minpoly_algHom (f : B →ₐ[A] B') f.injective x
-#align minpoly.minpoly_alg_equiv minpoly.minpoly_algEquiv
+theorem algEquiv_eq (f : B ≃ₐ[A] B') (x : B) : minpoly A (f x) = minpoly A x :=
+  algHom_eq (f : B →ₐ[A] B') f.injective x
+#align minpoly.minpoly_alg_equiv minpoly.algEquiv_eq
 
 variable (A x)
 

Mathlib/FieldTheory/Minpoly/Field.lean

@@ -126,21 +126,6 @@ theorem eq_of_irreducible [Nontrivial B] {p : A[X]} (hp1 : Irreducible p)
   · rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel]
 #align minpoly.eq_of_irreducible minpoly.eq_of_irreducible
 
-/-- If `y` is the image of `x` in an extension, their minimal polynomials coincide.
-
-We take `h : y = algebraMap L T x` as an argument because `rw h` typically fails
-since `IsIntegral R y` depends on y.
--/
-theorem eq_of_algebraMap_eq {K S T : Type*} [Field K] [CommRing S] [CommRing T] [Algebra K S]
-    [Algebra K T] [Algebra S T] [IsScalarTower K S T] (hST : Function.Injective (algebraMap S T))
-    {x : S} {y : T} (hx : IsIntegral K x) (h : y = algebraMap S T x) : minpoly K x = minpoly K y :=
-  minpoly.unique _ _ (minpoly.monic hx)
-    (by rw [h, aeval_algebraMap_apply, minpoly.aeval, RingHom.map_zero]) fun q q_monic root_q =>
-    minpoly.min _ _ q_monic
-      ((aeval_algebraMap_eq_zero_iff_of_injective hST).mp
-        (h ▸ root_q : Polynomial.aeval (algebraMap S T x) q = 0))
-#align minpoly.eq_of_algebra_map_eq minpoly.eq_of_algebraMap_eq
-
 theorem add_algebraMap {B : Type*} [CommRing B] [Algebra A B] {x : B} (hx : IsIntegral A x)
     (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

Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

@@ -50,8 +50,7 @@ polynomial over the fraction field. See `minpoly.isIntegrallyClosed_eq_field_fra
 theorem isIntegrallyClosed_eq_field_fractions [IsDomain S] {s : S} (hs : IsIntegral R s) :
     minpoly K (algebraMap S L s) = (minpoly R s).map (algebraMap R K) := by
   refine' (eq_of_irreducible_of_monic _ _ _).symm
-  · exact
-      (Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map (monic hs)).1 (irreducible hs)
+  · exact ((monic hs).irreducible_iff_irreducible_map_fraction_map).1 (irreducible hs)
   · rw [aeval_map_algebraMap, aeval_algebraMap_apply, aeval, map_zero]
   · exact (monic hs).map _
 #align minpoly.is_integrally_closed_eq_field_fractions minpoly.isIntegrallyClosed_eq_field_fractions
@@ -62,9 +61,7 @@ this version is useful if the element is in a ring that is already a `K`-algebra
 theorem isIntegrallyClosed_eq_field_fractions' [IsDomain S] [Algebra K S] [IsScalarTower R K S]
     {s : S} (hs : IsIntegral R s) : minpoly K s = (minpoly R s).map (algebraMap R K) := by
   let L := FractionRing S
-  rw [← isIntegrallyClosed_eq_field_fractions K L hs]
-  refine'
-    minpoly.eq_of_algebraMap_eq (IsFractionRing.injective S L) (isIntegral_of_isScalarTower hs) rfl
+  rw [← isIntegrallyClosed_eq_field_fractions K L hs, algebraMap_eq (IsFractionRing.injective S L)]
 #align minpoly.is_integrally_closed_eq_field_fractions' minpoly.isIntegrallyClosed_eq_field_fractions'
 
 end

Mathlib/FieldTheory/NormalClosure.lean

@@ -62,7 +62,7 @@ theorem restrictScalars_eq_iSup_adjoin [h : Normal F L] :
     -- Now it can't find a proof by unification, so we have to do it ourselves.
     apply PowerBasis.lift_gen
     change aeval y (minpoly F (AdjoinSimple.gen F x)) = 0
-    exact minpoly_gen (hi x) ▸ aeval_eq_zero_of_mem_rootSet (Multiset.mem_toFinset.mpr hy)
+    exact minpoly_gen F x ▸ aeval_eq_zero_of_mem_rootSet (Multiset.mem_toFinset.mpr hy)
 
 #align normal_closure.restrict_scalars_eq_supr_adjoin normalClosure.restrictScalars_eq_iSup_adjoin
 
@@ -74,8 +74,7 @@ instance normal [h : Normal F L] : Normal F (normalClosure F K L) := by
   intro x
   -- Porting note: use the `(_)` trick to obtain an instance by unification.
   apply Normal.of_isSplittingField (p := minpoly F x) (hFEp := _)
-  exact adjoin_rootSet_isSplittingField ((minpoly.eq_of_algebraMap_eq ϕ.injective
-    ((isIntegral_algebraMap_iff ϕ.injective).mp (h.isIntegral (ϕ x))) rfl).symm ▸ h.splits _)
+  exact adjoin_rootSet_isSplittingField (minpoly.algebraMap_eq ϕ.injective (A := F) x ▸ h.splits _)
 #align normal_closure.normal normalClosure.normal
 
 instance is_finiteDimensional [FiniteDimensional F K] :

Mathlib/LinearAlgebra/Matrix/Charpoly/Minpoly.lean

@@ -38,13 +38,13 @@ variable (M : Matrix n n R)
 
 @[simp]
 theorem minpoly_toLin' : minpoly R (toLin' M) = minpoly R M :=
-  minpoly.minpoly_algEquiv (toLinAlgEquiv' : Matrix n n R ≃ₐ[R] _) M
+  minpoly.algEquiv_eq (toLinAlgEquiv' : Matrix n n R ≃ₐ[R] _) M
 #align matrix.minpoly_to_lin' Matrix.minpoly_toLin'
 
 @[simp]
 theorem minpoly_toLin (b : Basis n R N) (M : Matrix n n R) :
     minpoly R (toLin b b M) = minpoly R M :=
-  minpoly.minpoly_algEquiv (toLinAlgEquiv b : Matrix n n R ≃ₐ[R] _) M
+  minpoly.algEquiv_eq (toLinAlgEquiv b : Matrix n n R ≃ₐ[R] _) M
 #align matrix.minpoly_to_lin Matrix.minpoly_toLin
 
 theorem isIntegral : IsIntegral R M :=
@@ -61,13 +61,13 @@ namespace LinearMap
 
 @[simp]
 theorem minpoly_toMatrix' (f : (n → R) →ₗ[R] n → R) : minpoly R (toMatrix' f) = minpoly R f :=
-  minpoly.minpoly_algEquiv (toMatrixAlgEquiv' : _ ≃ₐ[R] Matrix n n R) f
+  minpoly.algEquiv_eq (toMatrixAlgEquiv' : _ ≃ₐ[R] Matrix n n R) f
 #align linear_map.minpoly_to_matrix' LinearMap.minpoly_toMatrix'
 
 @[simp]
 theorem minpoly_toMatrix (b : Basis n R N) (f : N →ₗ[R] N) :
     minpoly R (toMatrix b b f) = minpoly R f :=
-  minpoly.minpoly_algEquiv (toMatrixAlgEquiv b : _ ≃ₐ[R] Matrix n n R) f
+  minpoly.algEquiv_eq (toMatrixAlgEquiv b : _ ≃ₐ[R] Matrix n n R) f
 #align linear_map.minpoly_to_matrix LinearMap.minpoly_toMatrix
 
 end LinearMap

Mathlib/RingTheory/Adjoin/PowerBasis.lean

@@ -37,16 +37,15 @@ noncomputable def adjoin.powerBasisAux {x : S} (hx : IsIntegral K x) :
     IsIntegral K (⟨x, subset_adjoin (Set.mem_singleton x)⟩ : adjoin K ({x} : Set S)) := by
     apply (isIntegral_algebraMap_iff hST).mp
     convert hx
-  have minpoly_eq := minpoly.eq_of_algebraMap_eq hST hx' rfl
   apply
     @Basis.mk (Fin (minpoly K x).natDegree) _ (adjoin K {x}) fun i =>
       ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ)
   · have : LinearIndependent K _ := linearIndependent_pow
       (⟨x, self_mem_adjoin_singleton _ _⟩ : adjoin K {x})
-    rwa [minpoly_eq] at this
+    rwa [← minpoly.algebraMap_eq hST] at this
   · rintro ⟨y, hy⟩ _
     have := hx'.mem_span_pow (y := ⟨y, hy⟩)
-    rw [minpoly_eq] at this
+    rw [← minpoly.algebraMap_eq hST] at this
     apply this
     · rw [adjoin_singleton_eq_range_aeval] at hy
       obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy

Mathlib/RingTheory/Norm.lean

@@ -233,13 +233,10 @@ theorem _root_.IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots (x : L)
   have injKxL := (algebraMap K⟮x⟯ L).injective
   by_cases hx : IsIntegral K x; swap
   · simp [minpoly.eq_zero hx, IntermediateField.AdjoinSimple.norm_gen_eq_one hx, aroots_def]
-  have hx' : IsIntegral K (AdjoinSimple.gen K x) := by
-    rwa [← isIntegral_algebraMap_iff injKxL, AdjoinSimple.algebraMap_gen]
   rw [← adjoin.powerBasis_gen hx, PowerBasis.norm_gen_eq_prod_roots] <;>
-  rw [adjoin.powerBasis_gen hx, minpoly.eq_of_algebraMap_eq injKxL hx'] <;>
-  try simp only [AdjoinSimple.algebraMap_gen _ _]
-  try exact hf
-  rfl
+    rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL] <;>
+    try simp only [AdjoinSimple.algebraMap_gen _ _]
+  exact hf
 #align intermediate_field.adjoin_simple.norm_gen_eq_prod_roots IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots
 
 end IntermediateField