chore: remove redundant integrality condition in IsSeparable (#8862)

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Author: alreadydone

Mathlib/FieldTheory/Fixed.lean

@@ -288,7 +288,7 @@ instance normal : Normal (FixedPoints.subfield G F) F :=
 #align fixed_points.normal FixedPoints.normal
 
 instance separable : IsSeparable (FixedPoints.subfield G F) F :=
-  ⟨isIntegral G F, fun x => by
+  ⟨fun x => by
     cases nonempty_fintype G
     -- this was a plain rw when we were using unbundled subrings
     erw [← minpoly_eq_minpoly, ← Polynomial.separable_map (FixedPoints.subfield G F).subtype,

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -204,8 +204,7 @@ instance (priority := 100) IsAlgClosure.normal (R K : Type*) [Field R] [Field K]
 
 instance (priority := 100) IsAlgClosure.separable (R K : Type*) [Field R] [Field K] [Algebra R K]
     [IsAlgClosure R K] [CharZero R] : IsSeparable R K :=
-  ⟨fun _ => (IsAlgClosure.algebraic _).isIntegral, fun _ =>
-    (minpoly.irreducible (IsAlgClosure.algebraic _).isIntegral).separable⟩
+  ⟨fun _ => (minpoly.irreducible (IsAlgClosure.algebraic _).isIntegral).separable⟩
 #align is_alg_closure.separable IsAlgClosure.separable
 
 namespace IsAlgClosed

Mathlib/FieldTheory/IsSepClosed.lean

@@ -193,7 +193,7 @@ instance isSeparable [Algebra k K] [IsSepClosure k K] : IsSeparable k K :=
   IsSepClosure.separable
 
 instance (priority := 100) normal [Algebra k K] [IsSepClosure k K] : Normal k K :=
-  ⟨fun x ↦ (IsSeparable.isIntegral' x).isAlgebraic,
+  ⟨fun x ↦ (IsSeparable.isIntegral k x).isAlgebraic,
     fun x ↦ (IsSepClosure.sep_closed k).splits_codomain _ (IsSeparable.separable k x)⟩
 
 end IsSepClosure
@@ -207,7 +207,7 @@ variable {K : Type u} {L : Type v} {M : Type w} [Field K] [Field L] [Algebra K L
   closed extension M of K. -/
 noncomputable irreducible_def lift : L →ₐ[K] M :=
   Classical.choice <| IntermediateField.nonempty_algHom_of_adjoin_splits
-    (fun x _ ↦ ⟨IsSeparable.isIntegral' x, splits_codomain _ (IsSeparable.separable K x)⟩)
+    (fun x _ ↦ ⟨IsSeparable.isIntegral K x, splits_codomain _ (IsSeparable.separable K x)⟩)
     (IntermediateField.adjoin_univ K L)
 
 end IsSepClosed

Mathlib/FieldTheory/Separable.lean

@@ -491,38 +491,40 @@ variable (F K : Type*) [CommRing F] [Ring K] [Algebra F K]
 -- is separable and normal, so if the definition of separable changes here at some point
 -- to allow non-algebraic extensions, then the definition of `IsGalois` must also be changed.
 /-- Typeclass for separable field extension: `K` is a separable field extension of `F` iff
-the minimal polynomial of every `x : K` is separable.
+the minimal polynomial of every `x : K` is separable. This implies that `K/F` is an algebraic
+extension, because the minimal polynomial of a non-integral element is 0, which is not
+separable.
 
 We define this for general (commutative) rings and only assume `F` and `K` are fields if this
 is needed for a proof.
 -/
-class IsSeparable : Prop where
-  isIntegral' (x : K) : IsIntegral F x
+@[mk_iff isSeparable_def] class IsSeparable : Prop where
   separable' (x : K) : (minpoly F x).Separable
 #align is_separable IsSeparable
 
 variable (F : Type*) {K : Type*} [CommRing F] [Ring K] [Algebra F K]
 
-theorem IsSeparable.isIntegral [IsSeparable F K] : ∀ x : K, IsIntegral F x :=
-  IsSeparable.isIntegral'
-#align is_separable.is_integral IsSeparable.isIntegral
-
 theorem IsSeparable.separable [IsSeparable F K] : ∀ x : K, (minpoly F x).Separable :=
   IsSeparable.separable'
 #align is_separable.separable IsSeparable.separable
 
+theorem IsSeparable.isIntegral [IsSeparable F K] : ∀ x : K, IsIntegral F x := fun x ↦ by
+  cases subsingleton_or_nontrivial F
+  · haveI := Module.subsingleton F K
+    exact ⟨1, monic_one, Subsingleton.elim _ _⟩
+  · exact of_not_not fun h ↦ not_separable_zero (minpoly.eq_zero h ▸ IsSeparable.separable F x)
+#align is_separable.is_integral IsSeparable.isIntegral
+
 variable {F K : Type*} [CommRing F] [Ring K] [Algebra F K]
 
 theorem isSeparable_iff : IsSeparable F K ↔ ∀ x : K, IsIntegral F x ∧ (minpoly F x).Separable :=
-  ⟨fun _ x => ⟨IsSeparable.isIntegral F x, IsSeparable.separable F x⟩, fun h =>
-    ⟨fun x => (h x).1, fun x => (h x).2⟩⟩
+  ⟨fun _ x => ⟨IsSeparable.isIntegral F x, IsSeparable.separable F x⟩, fun h => ⟨fun x => (h x).2⟩⟩
 #align is_separable_iff isSeparable_iff
 
 end CommRing
 
 instance isSeparable_self (F : Type*) [Field F] : IsSeparable F F :=
-  ⟨fun x => isIntegral_algebraMap,
-   fun x => by
+  ⟨fun x => by
     rw [minpoly.eq_X_sub_C']
     exact separable_X_sub_C⟩
 #align is_separable_self isSeparable_self
@@ -531,8 +533,7 @@ instance isSeparable_self (F : Type*) [Field F] : IsSeparable F F :=
 /-- A finite field extension in characteristic 0 is separable. -/
 instance (priority := 100) IsSeparable.of_finite (F K : Type*) [Field F] [Field K] [Algebra F K]
     [FiniteDimensional F K] [CharZero F] : IsSeparable F K :=
-  have : ∀ x : K, IsIntegral F x := fun _x ↦ .of_finite F _
-  ⟨this, fun x => (minpoly.irreducible (this x)).separable⟩
+  ⟨fun x => (minpoly.irreducible <| .of_finite F x).separable⟩
 #align is_separable.of_finite IsSeparable.of_finite
 
 section IsSeparableTower
@@ -541,18 +542,15 @@ variable (F K E : Type*) [Field F] [Field K] [Field E] [Algebra F K] [Algebra F
   [IsScalarTower F K E]
 
 theorem isSeparable_tower_top_of_isSeparable [IsSeparable F E] : IsSeparable K E :=
-  ⟨fun x ↦ (IsSeparable.isIntegral F x).tower_top, fun x ↦
-    (IsSeparable.separable F x).map.of_dvd (minpoly.dvd_map_of_isScalarTower _ _ _)⟩
+  ⟨fun x ↦ (IsSeparable.separable F x).map.of_dvd (minpoly.dvd_map_of_isScalarTower _ _ _)⟩
 #align is_separable_tower_top_of_is_separable isSeparable_tower_top_of_isSeparable
 
 theorem isSeparable_tower_bot_of_isSeparable [h : IsSeparable F E] : IsSeparable F K :=
-  isSeparable_iff.2 fun x ↦ by
-    refine (isSeparable_iff.1 h (algebraMap K E x)).imp .tower_bot_of_field fun hs ↦ ?_
-    obtain ⟨q, hq⟩ :=
+  ⟨fun x ↦
+    have ⟨_q, hq⟩ :=
       minpoly.dvd F x
         ((aeval_algebraMap_eq_zero_iff _ _ _).mp (minpoly.aeval F ((algebraMap K E) x)))
-    rw [hq] at hs
-    exact hs.of_mul_left
+    (hq ▸ h.separable (algebraMap K E x)).of_mul_left⟩
 #align is_separable_tower_bot_of_is_separable isSeparable_tower_bot_of_isSeparable
 
 variable {E}