chore: relax typeclass assumptions on Algebra.IsSeparable.of_finite (…

…#16791)
leanprover-community · Sep 15, 2024 · 2bac012 · 2bac012
1 parent cc716df
commit 2bac012
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/Mathlib/FieldTheory/Separable.lean b/Mathlib/FieldTheory/Separable.lean
@@ -579,10 +579,10 @@ instance Algebra.isSeparable_self (F : Type*) [Field F] : Algebra.IsSeparable F
     exact separable_X_sub_C⟩
 
 -- See note [lower instance priority]
-/-- A finite field extension in characteristic 0 is separable. -/
-instance (priority := 100) Algebra.IsSeparable.of_finite (F K : Type*) [Field F] [Field K]
-    [Algebra F K] [FiniteDimensional F K] [CharZero F] : Algebra.IsSeparable F K :=
-  ⟨fun x => (minpoly.irreducible <| .of_finite F x).separable⟩
+/-- An integral extension in characteristic 0 is separable. -/
+instance (priority := 100) Algebra.IsSeparable.of_integral (F K : Type*) [Field F] [Ring K]
+    [IsDomain K] [Algebra F K] [Algebra.IsIntegral F K] [CharZero F] : Algebra.IsSeparable F K :=
+  ⟨fun x => (minpoly.irreducible <| Algebra.IsIntegral.isIntegral x).separable⟩
 
 section IsSeparableTower