chore(FieldTheory/Adjoin): remove unnecessary assumptions in minpolynatDegree_le and minpoly.degree_le (#6152)

Also
- fix the names of `minpoly.natDegree_le` and  `minpoly.degree_le`
- rename `minpoly.ne_zero_of_finite_field_extension` to `minpoly.ne_zero_of_finite`
- reduce typeclass assumptions of some lemmas in `RingTheory/Algebraic`
- add two lemmas `isIntegral_of_finite` and `isAlgebraic_of_finite`
- move `Algebra.isIntegral_of_finite` to `RingTheory/IntegralClosure`

Author: astrainfinita

Mathlib/FieldTheory/Adjoin.lean

@@ -884,15 +884,16 @@ theorem adjoin.finrank {x : L} (hx : IsIntegral K x) :
   rfl
 #align intermediate_field.adjoin.finrank IntermediateField.adjoin.finrank
 
-theorem minpoly.natDegree_le {x : L} [FiniteDimensional K L] (hx : IsIntegral K x) :
+theorem _root_.minpoly.natDegree_le (x : L) [FiniteDimensional K L] :
     (minpoly K x).natDegree ≤ finrank K L :=
-  le_of_eq_of_le (IntermediateField.adjoin.finrank hx).symm K⟮x⟯.toSubmodule.finrank_le
-#align minpoly.nat_degree_le IntermediateField.minpoly.natDegree_le
+  le_of_eq_of_le (IntermediateField.adjoin.finrank (isIntegral_of_finite _ _)).symm
+    K⟮x⟯.toSubmodule.finrank_le
+#align minpoly.nat_degree_le minpoly.natDegree_le
 
-theorem minpoly.degree_le {x : L} [FiniteDimensional K L] (hx : IsIntegral K x) :
+theorem _root_.minpoly.degree_le (x : L) [FiniteDimensional K L] :
     (minpoly K x).degree ≤ finrank K L :=
-  degree_le_of_natDegree_le (minpoly.natDegree_le hx)
-#align minpoly.degree_le IntermediateField.minpoly.degree_le
+  degree_le_of_natDegree_le (minpoly.natDegree_le x)
+#align minpoly.degree_le minpoly.degree_le
 
 end PowerBasis
 

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -309,7 +309,7 @@ theorem maximalSubfieldWithHom_eq_top : (maximalSubfieldWithHom K L M).carrier =
   letI : Algebra N M := (maximalSubfieldWithHom K L M).emb.toRingHom.toAlgebra
   obtain ⟨y, hy⟩ := IsAlgClosed.exists_aeval_eq_zero M (minpoly N x) <|
     (minpoly.degree_pos
-      (isAlgebraic_iff_isIntegral.1 (Algebra.isAlgebraic_of_larger_base _ _ hL x))).ne'
+      (isAlgebraic_iff_isIntegral.1 (Algebra.isAlgebraic_of_larger_base _ hL x))).ne'
   let O : Subalgebra N L := Algebra.adjoin N {(x : L)}
   letI : Algebra N O := Subalgebra.algebra O
   -- Porting note: there are some tricky unfolds going on here:
@@ -549,7 +549,7 @@ theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly {F K} (A) [Field F] [F
   haveI : IsScalarTower F Fx A := IsScalarTower.of_ring_hom (AdjoinRoot.liftHom _ a ha)
   haveI : IsScalarTower F Fx K := IsScalarTower.of_ring_hom (AdjoinRoot.liftHom _ x hx)
   haveI : Fact (Irreducible <| minpoly F x) := ⟨minpoly.irreducible <| hFK x⟩
-  let ψ₀ : K →ₐ[Fx] A := IsAlgClosed.lift (Algebra.isAlgebraic_of_larger_base F Fx hK)
+  let ψ₀ : K →ₐ[Fx] A := IsAlgClosed.lift (Algebra.isAlgebraic_of_larger_base Fx hK)
   exact
     ⟨ψ₀.restrictScalars F,
       (congr_arg ψ₀ (AdjoinRoot.lift_root hx).symm).trans <|

Mathlib/FieldTheory/Minpoly/Field.lean

@@ -42,9 +42,9 @@ theorem degree_le_of_ne_zero {p : A[X]} (pnz : p ≠ 0) (hp : Polynomial.aeval x
     _ = degree p := degree_mul_leadingCoeff_inv p pnz
 #align minpoly.degree_le_of_ne_zero minpoly.degree_le_of_ne_zero
 
-theorem ne_zero_of_finite_field_extension (e : B) [FiniteDimensional A B] : minpoly A e ≠ 0 :=
-  minpoly.ne_zero <| isIntegral_of_noetherian (IsNoetherian.iff_fg.2 inferInstance) _
-#align minpoly.ne_zero_of_finite_field_extension minpoly.ne_zero_of_finite_field_extension
+theorem ne_zero_of_finite (e : B) [FiniteDimensional A B] : minpoly A e ≠ 0 :=
+  minpoly.ne_zero <| isIntegral_of_finite _ _
+#align minpoly.ne_zero_of_finite_field_extension minpoly.ne_zero_of_finite
 
 /-- The minimal polynomial of an element `x` is uniquely characterized by its defining property:
 if there is another monic polynomial of minimal degree that has `x` as a root, then this polynomial
@@ -178,7 +178,7 @@ def rootsOfMinPolyPiType (φ : E →ₐ[F] K)
     (x : range (FiniteDimensional.finBasis F E : _ → E)) :
     { l : K // l ∈ (((minpoly F x.1).map (algebraMap F K)).roots : Multiset K) } :=
   ⟨φ x, by
-    rw [mem_roots_map (minpoly.ne_zero_of_finite_field_extension F x.val),
+    rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val),
       ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]⟩
 #align minpoly.roots_of_min_poly_pi_type minpoly.rootsOfMinPolyPiType
 

Mathlib/NumberTheory/NumberField/Embeddings.lean

@@ -89,7 +89,7 @@ theorem coeff_bdd_of_norm_le {B : ℝ} {x : K} (h : ∀ φ : K →+* A, ‖φ x
   have hx := IsSeparable.isIntegral ℚ x
   rw [← norm_algebraMap' A, ← coeff_map (algebraMap ℚ A)]
   refine coeff_bdd_of_roots_le _ (minpoly.monic hx)
-      (IsAlgClosed.splits_codomain _) (IntermediateField.minpoly.natDegree_le hx) (fun z hz => ?_) i
+      (IsAlgClosed.splits_codomain _) (minpoly.natDegree_le x) (fun z hz => ?_) i
   classical
   rw [← Multiset.mem_toFinset] at hz
   obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz
@@ -107,7 +107,7 @@ theorem finite_of_norm_le (B : ℝ) : {x : K | IsIntegral ℤ x ∧ ∀ φ : K 
   have h_map_ℚ_minpoly := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx.1
   refine ⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩
   · rw [← (minpoly.monic hx.1).natDegree_map (algebraMap ℤ ℚ), ← h_map_ℚ_minpoly]
-    exact IntermediateField.minpoly.natDegree_le (isIntegral_of_isScalarTower hx.1)
+    exact minpoly.natDegree_le x
   rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ]
   refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)
   rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]

Mathlib/RingTheory/Algebraic.lean

@@ -199,67 +199,95 @@ protected theorem Algebra.isAlgebraic_iff_isIntegral :
 
 end Field
 
-namespace Algebra
+section
 
 variable {K : Type _} {L : Type _} {R : Type _} {S : Type _} {A : Type _}
 
-variable [Field K] [Field L] [CommRing R] [CommRing S] [CommRing A]
+section Ring
 
-variable [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A]
+section CommRing
 
-variable [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A]
+variable [CommRing R] [CommRing S] [Ring A]
 
-/-- If L is an algebraic field extension of K and A is an algebraic algebra over L,
-then A is algebraic over K. -/
-theorem isAlgebraic_trans (L_alg : IsAlgebraic K L) (A_alg : IsAlgebraic L A) :
-    IsAlgebraic K A := by
-  simp only [IsAlgebraic, isAlgebraic_iff_isIntegral] at L_alg A_alg ⊢
-  exact isIntegral_trans L_alg A_alg
-#align algebra.is_algebraic_trans Algebra.isAlgebraic_trans
-
-variable (K L)
+variable [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A]
 
 /-- If x is algebraic over R, then x is algebraic over S when S is an extension of R,
   and the map from `R` to `S` is injective. -/
-theorem _root_.isAlgebraic_of_larger_base_of_injective
+theorem isAlgebraic_of_larger_base_of_injective
     (hinj : Function.Injective (algebraMap R S)) {x : A}
-    (A_alg : _root_.IsAlgebraic R x) : _root_.IsAlgebraic S x :=
+    (A_alg : IsAlgebraic R x) : IsAlgebraic S x :=
   let ⟨p, hp₁, hp₂⟩ := A_alg
   ⟨p.map (algebraMap _ _), by
     rwa [Ne.def, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot], by simpa⟩
 #align is_algebraic_of_larger_base_of_injective isAlgebraic_of_larger_base_of_injective
 
 /-- If A is an algebraic algebra over R, then A is algebraic over S when S is an extension of R,
   and the map from `R` to `S` is injective. -/
-theorem isAlgebraic_of_larger_base_of_injective (hinj : Function.Injective (algebraMap R S))
+theorem Algebra.isAlgebraic_of_larger_base_of_injective (hinj : Function.Injective (algebraMap R S))
     (A_alg : IsAlgebraic R A) : IsAlgebraic S A := fun x =>
   _root_.isAlgebraic_of_larger_base_of_injective hinj (A_alg x)
 #align algebra.is_algebraic_of_larger_base_of_injective Algebra.isAlgebraic_of_larger_base_of_injective
 
+end CommRing
+
+section Field
+
+variable [Field K] [Field L] [Ring A]
+
+variable [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A]
+
+variable (L)
+
 /-- If x is algebraic over K, then x is algebraic over L when L is an extension of K -/
-theorem _root_.isAlgebraic_of_larger_base {x : A} (A_alg : _root_.IsAlgebraic K x) :
-    _root_.IsAlgebraic L x :=
-  _root_.isAlgebraic_of_larger_base_of_injective (algebraMap K L).injective A_alg
+theorem isAlgebraic_of_larger_base {x : A} (A_alg : IsAlgebraic K x) :
+    IsAlgebraic L x :=
+  isAlgebraic_of_larger_base_of_injective (algebraMap K L).injective A_alg
 #align is_algebraic_of_larger_base isAlgebraic_of_larger_base
 
 /-- If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K -/
-theorem isAlgebraic_of_larger_base (A_alg : IsAlgebraic K A) : IsAlgebraic L A :=
+theorem Algebra.isAlgebraic_of_larger_base (A_alg : IsAlgebraic K A) : IsAlgebraic L A :=
   isAlgebraic_of_larger_base_of_injective (algebraMap K L).injective A_alg
 #align algebra.is_algebraic_of_larger_base Algebra.isAlgebraic_of_larger_base
 
-/-- A field extension is integral if it is finite. -/
-theorem isIntegral_of_finite [FiniteDimensional K L] : Algebra.IsIntegral K L := fun x =>
-  isIntegral_of_submodule_noetherian ⊤ (IsNoetherian.iff_fg.2 inferInstance) x Algebra.mem_top
-#align algebra.is_integral_of_finite Algebra.isIntegral_of_finite
+variable (K)
+
+theorem isAlgebraic_of_finite (e : A) [FiniteDimensional K A] : IsAlgebraic K e :=
+  isAlgebraic_iff_isIntegral.mpr (isIntegral_of_finite K e)
+
+variable (A)
 
 /-- A field extension is algebraic if it is finite. -/
-theorem isAlgebraic_of_finite [FiniteDimensional K L] : IsAlgebraic K L :=
-  Algebra.isAlgebraic_iff_isIntegral.mpr (isIntegral_of_finite K L)
+theorem Algebra.isAlgebraic_of_finite [FiniteDimensional K A] : IsAlgebraic K A :=
+  Algebra.isAlgebraic_iff_isIntegral.mpr (isIntegral_of_finite K A)
 #align algebra.is_algebraic_of_finite Algebra.isAlgebraic_of_finite
 
-variable {K L}
+end Field
+
+end Ring
+
+section CommRing
+
+variable [Field K] [Field L] [CommRing A]
+
+variable [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A]
 
-theorem IsAlgebraic.algHom_bijective (ha : Algebra.IsAlgebraic K L) (f : L →ₐ[K] L) :
+/-- If L is an algebraic field extension of K and A is an algebraic algebra over L,
+then A is algebraic over K. -/
+theorem Algebra.isAlgebraic_trans (L_alg : IsAlgebraic K L) (A_alg : IsAlgebraic L A) :
+    IsAlgebraic K A := by
+  simp only [IsAlgebraic, isAlgebraic_iff_isIntegral] at L_alg A_alg ⊢
+  exact isIntegral_trans L_alg A_alg
+#align algebra.is_algebraic_trans Algebra.isAlgebraic_trans
+
+end CommRing
+
+section Field
+
+variable [Field K] [Field L]
+
+variable [Algebra K L]
+
+theorem Algebra.IsAlgebraic.algHom_bijective (ha : Algebra.IsAlgebraic K L) (f : L →ₐ[K] L) :
     Function.Bijective f := by
   refine' ⟨f.toRingHom.injective, fun b => _⟩
   obtain ⟨p, hp, he⟩ := ha b
@@ -271,15 +299,15 @@ theorem IsAlgebraic.algHom_bijective (ha : Algebra.IsAlgebraic K L) (f : L →
   exact ⟨a, Subtype.ext_iff.1 ha⟩
 #align algebra.is_algebraic.alg_hom_bijective Algebra.IsAlgebraic.algHom_bijective
 
-theorem _root_.AlgHom.bijective [FiniteDimensional K L] (ϕ : L →ₐ[K] L) : Function.Bijective ϕ :=
+theorem AlgHom.bijective [FiniteDimensional K L] (ϕ : L →ₐ[K] L) : Function.Bijective ϕ :=
   (Algebra.isAlgebraic_of_finite K L).algHom_bijective ϕ
 #align alg_hom.bijective AlgHom.bijective
 
 variable (K L)
 
 /-- Bijection between algebra equivalences and algebra homomorphisms -/
 @[simps]
-noncomputable def IsAlgebraic.algEquivEquivAlgHom (ha : Algebra.IsAlgebraic K L) :
+noncomputable def Algebra.IsAlgebraic.algEquivEquivAlgHom (ha : Algebra.IsAlgebraic K L) :
     (L ≃ₐ[K] L) ≃* (L →ₐ[K] L) where
   toFun ϕ := ϕ.toAlgHom
   invFun ϕ := AlgEquiv.ofBijective ϕ (ha.algHom_bijective ϕ)
@@ -294,12 +322,14 @@ noncomputable def IsAlgebraic.algEquivEquivAlgHom (ha : Algebra.IsAlgebraic K L)
 
 /-- Bijection between algebra equivalences and algebra homomorphisms -/
 @[reducible]
-noncomputable def _root_.algEquivEquivAlgHom [FiniteDimensional K L] :
+noncomputable def algEquivEquivAlgHom [FiniteDimensional K L] :
     (L ≃ₐ[K] L) ≃* (L →ₐ[K] L) :=
   (Algebra.isAlgebraic_of_finite K L).algEquivEquivAlgHom K L
 #align alg_equiv_equiv_alg_hom algEquivEquivAlgHom
 
-end Algebra
+end Field
+
+end
 
 variable {R S : Type _} [CommRing R] [IsDomain R] [CommRing S]
 

Mathlib/RingTheory/IntegralClosure.lean

@@ -115,6 +115,26 @@ end Ring
 
 section
 
+variable {K A : Type _}
+
+variable [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A]
+
+variable (K)
+
+theorem isIntegral_of_finite (e : A) : IsIntegral K e :=
+  isIntegral_of_noetherian (IsNoetherian.iff_fg.2 inferInstance) _
+
+variable (A)
+
+/-- A field extension is integral if it is finite. -/
+theorem Algebra.isIntegral_of_finite : Algebra.IsIntegral K A := fun x =>
+  isIntegral_of_submodule_noetherian ⊤ (IsNoetherian.iff_fg.2 inferInstance) x Algebra.mem_top
+#align algebra.is_integral_of_finite Algebra.isIntegral_of_finite
+
+end
+
+section
+
 variable {R A B S : Type _}
 
 variable [CommRing R] [CommRing A] [CommRing B] [CommRing S]