# Separable polynomials #

We define a polynomial to be separable if it is coprime with its derivative. We prove basic properties about separable polynomials here.

## Main definitions #

- `Polynomial.Separable f`: a polynomial `f` is separable iff it is coprime with its derivative.
- `IsSeparable K x`: an element `x` is separable over `K` iff the minimal polynomial of `x` over `K` is separable.
- `Algebra.IsSeparable K L`: `L` is separable over `K` iff every element in `L` is separable over `K`.

source
def Polynomial.Separable {R : Type u} [CommSemiring R] (f : Polynomial R) :
Prop

A polynomial is separable iff it is coprime with its derivative.

Equations

- f.Separable = IsCoprime f (Polynomial.derivative f)

Instances For

source
theorem Polynomial.separable_def {R : Type u} [CommSemiring R] (f : Polynomial R) :
f.Separable ↔ IsCoprime f (derivative f)
source
theorem Polynomial.separable_def' {R : Type u} [CommSemiring R] (f : Polynomial R) :
f.Separable ↔ ∃ (a : Polynomial R) (b : Polynomial R), a * f + b * derivative f = 1
source
theorem Polynomial.not_separable_zero {R : Type u} [CommSemiring R] [Nontrivial R] :
¬Separable 0
source
theorem Polynomial.Separable.ne_zero {R : Type u} [CommSemiring R] [Nontrivial R] {f : Polynomial R} (h : f.Separable) :
f ≠ 0
source
@[simp]
theorem Polynomial.separable_one {R : Type u} [CommSemiring R] :
Separable 1
source
theorem Polynomial.separable_of_subsingleton {R : Type u} [CommSemiring R] [Subsingleton R] (f : Polynomial R) :
f.Separable
source
theorem Polynomial.separable_X_add_C {R : Type u} [CommSemiring R] (a : R) :
(X + C a).Separable
source
theorem Polynomial.separable_X {R : Type u} [CommSemiring R] :
X.Separable
source
theorem Polynomial.separable_C {R : Type u} [CommSemiring R] (r : R) :
(C r).Separable ↔ IsUnit r
source
theorem Polynomial.Separable.of_mul_left {R : Type u} [CommSemiring R] {f g : Polynomial R} (h : (f * g).Separable) :
f.Separable
source
theorem Polynomial.Separable.of_mul_right {R : Type u} [CommSemiring R] {f g : Polynomial R} (h : (f * g).Separable) :
g.Separable
source
theorem Polynomial.Separable.of_dvd {R : Type u} [CommSemiring R] {f g : Polynomial R} (hf : f.Separable) (hfg : g ∣ f) :
g.Separable
source
theorem Polynomial.separable_gcd_left {F : Type u_1} [Field F] [DecidableEq (Polynomial F)] {f : Polynomial F} (hf : f.Separable) (g : Polynomial F) :
(EuclideanDomain.gcd f g).Separable
source
theorem Polynomial.separable_gcd_right {F : Type u_1} [Field F] [DecidableEq (Polynomial F)] {g : Polynomial F} (f : Polynomial F) (hg : g.Separable) :
(EuclideanDomain.gcd f g).Separable
source
theorem Polynomial.Separable.isCoprime {R : Type u} [CommSemiring R] {f g : Polynomial R} (h : (f * g).Separable) :
IsCoprime f g
source
theorem Polynomial.Separable.of_pow' {R : Type u} [CommSemiring R] {f : Polynomial R} {n : ℕ} (_h : (f ^ n).Separable) :
IsUnit f ∨ f.Separable ∧ n = 1 ∨ n = 0
source
theorem Polynomial.Separable.of_pow {R : Type u} [CommSemiring R] {f : Polynomial R} (hf : ¬IsUnit f) {n : ℕ} (hn : n ≠ 0) (hfs : (f ^ n).Separable) :
f.Separable ∧ n = 1
source
theorem Polynomial.Separable.map {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] {p : Polynomial R} (h : p.Separable) {f : R →+* S} :
(Polynomial.map f p).Separable
source
theorem Associated.separable {R : Type u} [CommSemiring R] {f g : Polynomial R} (ha : Associated f g) (h : f.Separable) :
g.Separable
source
theorem Associated.separable_iff {R : Type u} [CommSemiring R] {f g : Polynomial R} (ha : Associated f g) :
f.Separable ↔ g.Separable
source
theorem Polynomial.Separable.mul_unit {R : Type u} [CommSemiring R] {f g : Polynomial R} (hf : f.Separable) (hg : IsUnit g) :
(f * g).Separable
source
theorem Polynomial.Separable.unit_mul {R : Type u} [CommSemiring R] {f g : Polynomial R} (hf : IsUnit f) (hg : g.Separable) :
(f * g).Separable
source
theorem Polynomial.Separable.eval₂_derivative_ne_zero {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] [Nontrivial S] (f : R →+* S) {p : Polynomial R} (h : p.Separable) {x : S} (hx : eval₂ f x p = 0) :
eval₂ f x (derivative p) ≠ 0
source
theorem Polynomial.Separable.aeval_derivative_ne_zero {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] [Nontrivial S] [Algebra R S] {p : Polynomial R} (h : p.Separable) {x : S} (hx : (aeval x) p = 0) :
(aeval x) (derivative p) ≠ 0
source
theorem Polynomial.isUnit_of_self_mul_dvd_separable {R : Type u} [CommSemiring R] {p q : Polynomial R} (hp : p.Separable) (hq : q * q ∣ p) :
IsUnit q
source
theorem Polynomial.emultiplicity_le_one_of_separable {R : Type u} [CommSemiring R] {p q : Polynomial R} (hq : ¬IsUnit q) (hsep : p.Separable) :
emultiplicity q p ≤ 1
source
theorem Polynomial.Separable.squarefree {R : Type u} [CommSemiring R] {p : Polynomial R} (hsep : p.Separable) :
Squarefree p

A separable polynomial is square-free.

See `PerfectField.separable_iff_squarefree` for the converse when the coefficients are a perfect field.

source
theorem Polynomial.separable_X_sub_C {R : Type u} [CommRing R] {x : R} :
(X - C x).Separable
source
theorem Polynomial.Separable.mul {R : Type u} [CommRing R] {f g : Polynomial R} (hf : f.Separable) (hg : g.Separable) (h : IsCoprime f g) :
(f * g).Separable
source
theorem Polynomial.separable_prod' {R : Type u} [CommRing R] {ι : Type u_1} {f : ι → Polynomial R} {s : Finset ι} :
(∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
source
theorem Polynomial.separable_prod {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {f : ι → Polynomial R} (h1 : Pairwise (Function.onFun IsCoprime f)) (h2 : ∀ (x : ι), (f x).Separable) :
(∏ x : ι, f x).Separable
source
theorem Polynomial.Separable.inj_of_prod_X_sub_C {R : Type u} [CommRing R] [Nontrivial R] {ι : Type u_1} {f : ι → R} {s : Finset ι} (hfs : (∏ i ∈ s, (X - C (f i))).Separable) {x y : ι} (hx : x ∈ s) (hy : y ∈ s) (hfxy : f x = f y) :
x = y
source
theorem Polynomial.Separable.injective_of_prod_X_sub_C {R : Type u} [CommRing R] [Nontrivial R] {ι : Type u_1} [Fintype ι] {f : ι → R} (hfs : (∏ i : ι, (X - C (f i))).Separable) :
Function.Injective f
source
theorem Polynomial.nodup_of_separable_prod {R : Type u} [CommRing R] [Nontrivial R] {s : Multiset R} (hs : (Multiset.map (fun (a : R) => X - C a) s).prod.Separable) :
s.Nodup
source
theorem Polynomial.separable_X_pow_sub_C_unit {R : Type u} [CommRing R] {n : ℕ} (u : R ˣ) (hn : IsUnit ↑n) :
(X ^ n - C ↑u).Separable

If `IsUnit n` in a `CommRing R`, then `X ^ n - u` is separable for any unit `u`.

source
theorem Polynomial.separable_C_mul_X_pow_add_C_mul_X_add_C {R : Type u} [CommRing R] {n : ℕ} (a b c : R) (hn : ↑n = 0) (hb : IsUnit b) :
(C a * X ^ n + C b * X + C c).Separable

If `n = 0` in `R` and `b` is a unit, then `a * X ^ n + b * X + c` is separable.

source
theorem Polynomial.separable_C_mul_X_pow_add_C_mul_X_add_C' {R : Type u} [CommRing R] (p n : ℕ) (a b c : R) [CharP R p] (hn : p ∣ n) (hb : IsUnit b) :
(C a * X ^ n + C b * X + C c).Separable

If `R` is of characteristic `p`, `p ∣ n` and `b` is a unit, then `a * X ^ n + b * X + c` is separable.

source
theorem Polynomial.rootMultiplicity_le_one_of_separable {R : Type u} [CommRing R] [Nontrivial R] {p : Polynomial R} (hsep : p.Separable) (x : R) :
rootMultiplicity x p ≤ 1
source
theorem Polynomial.count_roots_le_one {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] {p : Polynomial R} (hsep : p.Separable) (x : R) :
Multiset.count x p.roots ≤ 1
source
theorem Polynomial.nodup_roots {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hsep : p.Separable) :
p.roots.Nodup
source
theorem Polynomial.separable_iff_derivative_ne_zero {F : Type u} [Field F] {f : Polynomial F} (hf : Irreducible f) :
f.Separable ↔ derivative f ≠ 0
source
theorem Polynomial.separable_map {F : Type u} [Field F] {S : Type u_1} [CommRing S] [Nontrivial S] (f : F →+* S) {p : Polynomial F} :
(map f p).Separable ↔ p.Separable
source
theorem Polynomial.separable_prod_X_sub_C_iff' {F : Type u} [Field F] {ι : Type u_1} {f : ι → F} {s : Finset ι} :
(∏ i ∈ s, (X - C (f i))).Separable ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
source
theorem Polynomial.separable_prod_X_sub_C_iff {F : Type u} [Field F] {ι : Type u_1} [Fintype ι] {f : ι → F} :
(∏ i : ι, (X - C (f i))).Separable ↔ Function.Injective f
source
theorem Polynomial.separable_or {F : Type u} [Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F} (hf : Irreducible f) :
f.Separable ∨ ¬f.Separable ∧ ∃ (g : Polynomial F), Irreducible g ∧ (expand F p) g = f
source
theorem Polynomial.exists_separable_of_irreducible {F : Type u} [Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F} (hf : Irreducible f) (hp : p ≠ 0) :
∃ (n : ℕ) (g : Polynomial F), g.Separable ∧ (expand F (p ^ n)) g = f
source
theorem Polynomial.isUnit_or_eq_zero_of_separable_expand {F : Type u} [Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F} (n : ℕ) (hp : 0 < p) (hf : ((expand F (p ^ n)) f).Separable) :
IsUnit f ∨ n = 0
source
theorem Polynomial.unique_separable_of_irreducible {F : Type u} [Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F} (hf : Irreducible f) (hp : 0 < p) (n₁ : ℕ) (g₁ : Polynomial F) (hg₁ : g₁.Separable) (hgf₁ : (expand F (p ^ n₁)) g₁ = f) (n₂ : ℕ) (g₂ : Polynomial F) (hg₂ : g₂.Separable) (hgf₂ : (expand F (p ^ n₂)) g₂ = f) :
n₁ = n₂ ∧ g₁ = g₂
source
theorem Polynomial.separable_X_pow_sub_C {F : Type u} [Field F] {n : ℕ} (a : F) (hn : ↑n ≠ 0) (ha : a ≠ 0) :
(X ^ n - C a).Separable

If `n ≠ 0` in `F`, then `X ^ n - a` is separable for any `a ≠ 0`.

source
theorem Polynomial.separable_X_pow_sub_C' {F : Type u} [Field F] (p n : ℕ) (a : F) [CharP F p] (hn : ¬p ∣ n) (ha : a ≠ 0) :
(X ^ n - C a).Separable

If `F` is of characteristic `p` and `p ∤ n`, then `X ^ n - a` is separable for any `a ≠ 0`.

source
theorem Polynomial.X_pow_sub_one_separable_iff {F : Type u} [Field F] {n : ℕ} :
(X ^ n - 1).Separable ↔ ↑n ≠ 0

In a field `F`, `X ^ n - 1` is separable iff `↑n ≠ 0`.

source
theorem Polynomial.card_rootSet_eq_natDegree {F : Type u} [Field F] {K : Type v} [Field K] [Algebra F K] {p : Polynomial F} (hsep : p.Separable) (hsplit : Splits (algebraMap F K) p) :
Fintype.card ↑(p.rootSet K) = p.natDegree
source
theorem Polynomial.nodup_roots_iff_of_splits {F : Type u} [Field F] {f : Polynomial F} (hf : f ≠ 0) (h : Splits (RingHom.id F) f) :
f.roots.Nodup ↔ f.Separable

If a non-zero polynomial splits, then it has no repeated roots on that field if and only if it is separable.

source
theorem Polynomial.nodup_aroots_iff_of_splits {F : Type u} [Field F] {K : Type v} [Field K] [Algebra F K] {f : Polynomial F} (hf : f ≠ 0) (h : Splits (algebraMap F K) f) :
(f.aroots K).Nodup ↔ f.Separable

If a non-zero polynomial over `F` splits in `K`, then it has no repeated roots on `K` if and only if it is separable.

source
theorem Polynomial.card_rootSet_eq_natDegree_iff_of_splits {F : Type u} [Field F] {K : Type v} [Field K] [Algebra F K] {f : Polynomial F} (hf : f ≠ 0) (h : Splits (algebraMap F K) f) :
Fintype.card ↑(f.rootSet K) = f.natDegree ↔ f.Separable
source
theorem Polynomial.eq_X_sub_C_of_separable_of_root_eq {F : Type u} [Field F] {K : Type v} [Field K] {i : F →+* K} {x : F} {h : Polynomial F} (h_sep : h.Separable) (h_root : eval x h = 0) (h_splits : Splits i h) (h_roots : ∀ y ∈ (map i h).roots, y = i x) :
h = C h.leadingCoeff * (X - C x)
source
theorem Polynomial.exists_finset_of_splits {F : Type u} [Field F] {K : Type v} [Field K] (i : F →+* K) {f : Polynomial F} (sep : f.Separable) (sp : Splits i f) :
∃ (s : Finset K), map i f = C (i f.leadingCoeff) * ∏ a ∈ s, (X - C a)
source
theorem Irreducible.separable {F : Type u} [Field F] [CharZero F] {f : Polynomial F} (hf : Irreducible f) :
f.Separable
source
def IsSeparable (F : Type u_1) {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] (x : K) :
Prop

An element `x` of an algebra `K` over a commutative ring `F` is said to be separable, if its minimal polynomial over `K` is separable. Note that the minimal polynomial of any element not integral over `F` is defined to be `0`, which is not a separable polynomial.

Equations

- IsSeparable F x = (minpoly F x).Separable

Instances For

source
class Algebra.IsSeparable (F : Type u_1) (K : Type u_3) [CommRing F] [Ring K] [Algebra F K] :
Prop

Typeclass for separable field extension: `K` is a separable field extension of `F` iff 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.

- isSeparable' (x : K) : IsSeparable F x

Instances

source
theorem Algebra.isSeparable_def (F : Type u_1) (K : Type u_3) [CommRing F] [Ring K] [Algebra F K] :
Algebra.IsSeparable F K ↔ ∀ (x : K), IsSeparable F x
source
theorem Algebra.IsSeparable.isSeparable (F : Type u_1) {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] [Algebra.IsSeparable F K] (x : K) :
IsSeparable F x
source
theorem IsSeparable.isIntegral {F : Type u_1} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] {x : K} (h : IsSeparable F x) :
IsIntegral F x

If the minimal polynomial of `x : K` over `F` is separable, then `x` is integral over `F`, because the minimal polynomial of a non-integral element is `0`, which is not separable.

source
theorem Algebra.IsSeparable.isIntegral (F : Type u_1) {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] [Algebra.IsSeparable F K] (x : K) :
IsIntegral F x
source
instance Algebra.IsSeparable.isAlgebraic (F : Type u_1) (K : Type u_3) [CommRing F] [Ring K] [Algebra F K] [Nontrivial F] [Algebra.IsSeparable F K] :
Algebra.IsAlgebraic F K
source
theorem Algebra.isSeparable_iff {F : Type u_1} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] :
Algebra.IsSeparable F K ↔ ∀ (x : K), IsIntegral F x ∧ IsSeparable F x
source
theorem IsSeparable.map {F : Type u_1} {L : Type u_2} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] [Ring L] [Algebra F L] {x : K} (f : K →ₐ[F] L) (hf : Function.Injective ⇑f) (H : IsSeparable F x) :
IsSeparable F (f x)
source
theorem AlgEquiv.isSeparable_iff {F : Type u_1} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] {E : Type u_4} [Ring E] [Algebra F E] (e : K ≃ₐ[F] E) {x : K} :
IsSeparable F (e x) ↔ IsSeparable F x

Transfer `IsSeparable` across an `AlgEquiv`.

source
theorem AlgEquiv.Algebra.isSeparable {F : Type u_1} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] {E : Type u_4} [Ring E] [Algebra F E] (e : K ≃ₐ[F] E) [Algebra.IsSeparable F K] :
Algebra.IsSeparable F E

Transfer `Algebra.IsSeparable` across an `AlgEquiv`.

source
theorem AlgEquiv.Algebra.isSeparable_iff {F : Type u_1} {K : Type u_3} [CommRing F] [Ring K] [Algebra F K] {E : Type u_4} [Ring E] [Algebra F E] (e : K ≃ₐ[F] E) :
Algebra.IsSeparable F K ↔ Algebra.IsSeparable F E
source
theorem IsSeparable.tower_top {F : Type u_1} (L : Type u_2) [CommRing F] {E : Type u_4} [Field L] [Ring E] [Algebra F L] [Algebra F E] [Algebra L E] [IsScalarTower F L E] {x : E} (h : IsSeparable F x) :
IsSeparable L x

If `E / L / F` is a scalar tower and `x : E` is separable over `F`, then it's also separable over `L`.

source
theorem Algebra.isSeparable_tower_top_of_isSeparable (F : Type u_1) (L : Type u_2) [CommRing F] (E : Type u_4) [Field L] [Ring E] [Algebra F L] [Algebra F E] [Algebra L E] [IsScalarTower F L E] [Algebra.IsSeparable F E] :
Algebra.IsSeparable L E

If `E / K / F` is an extension tower, `E` is separable over `F`, then it's also separable over `K`.

source
theorem isSeparable_algebraMap {F : Type u_1} [Field F] {K : Type u_2} [Ring K] [Algebra F K] (x : F) :
IsSeparable F ((algebraMap F K) x)
source
instance Algebra.isSeparable_self (F : Type u_1) [Field F] :
Algebra.IsSeparable F F
source
theorem IsSeparable.of_integral (F : Type u_1) [Field F] {K : Type u_2} [Ring K] [Algebra F K] [IsDomain K] [Algebra.IsIntegral F K] [CharZero F] (x : K) :
IsSeparable F x
source
@[instance 100]
instance Algebra.IsSeparable.of_integral (F : Type u_1) [Field F] (K : Type u_2) [Ring K] [Algebra F K] [IsDomain K] [Algebra.IsIntegral F K] [CharZero F] :
Algebra.IsSeparable F K

A integral field extension in characteristic 0 is separable.

source
theorem IsSeparable.tower_bot {F : Type u_1} [Field F] {K : Type u_2} {E : Type u_3} [Field K] [Ring E] [Algebra F K] [Algebra F E] [Algebra K E] [Nontrivial E] [IsScalarTower F K E] {x : K} (h : IsSeparable F ((algebraMap K E) x)) :
IsSeparable F x

If `E / K / F` is a scalar tower and `algebraMap K E x` is separable over `F`, then `x` is also separable over `F`.

source
theorem Algebra.isSeparable_tower_bot_of_isSeparable (F : Type u_1) [Field F] (K : Type u_2) (E : Type u_3) [Field K] [Ring E] [Algebra F K] [Algebra F E] [Algebra K E] [Nontrivial E] [IsScalarTower F K E] [h : Algebra.IsSeparable F E] :
Algebra.IsSeparable F K
source
theorem IsSeparable.of_algHom {F : Type u_1} [Field F] {E : Type u_3} {E' : Type u_4} [Field E] [Field E'] [Algebra F E] [Algebra F E'] (f : E →ₐ[F] E') {x : E} (h : IsSeparable F (f x)) :
IsSeparable F x
source
theorem Algebra.IsSeparable.of_algHom (F : Type u_1) [Field F] {E : Type u_3} (E' : Type u_4) [Field E] [Field E'] [Algebra F E] [Algebra F E'] (f : E →ₐ[F] E') [Algebra.IsSeparable F E'] :
Algebra.IsSeparable F E
source
instance IntermediateField.isSeparable_tower_bot (F : Type u_1) [Field F] {K : Type u_2} [Field K] [Algebra F K] (M : IntermediateField F K) [Algebra.IsSeparable F K] :
Algebra.IsSeparable F ↥M
source
instance IntermediateField.isSeparable_tower_top (F : Type u_1) [Field F] {K : Type u_2} [Field K] [Algebra F K] (M : IntermediateField F K) [Algebra.IsSeparable F K] :
Algebra.IsSeparable (↥M) K
source
theorem IsSeparable.of_equiv_equiv {A₁ : Type u_1} {B₁ : Type u_2} {A₂ : Type u_3} {B₂ : Type u_4} [Field A₁] [Ring B₁] [Field A₂] [Ring B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂) (he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)) {x : B₁} (h : IsSeparable A₁ x) :
IsSeparable A₂ (e₂ x)
source
theorem Algebra.IsSeparable.of_equiv_equiv {A₁ : Type u_1} {B₁ : Type u_2} {A₂ : Type u_3} {B₂ : Type u_4} [Field A₁] [Ring B₁] [Field A₂] [Ring B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂) (he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)) [Algebra.IsSeparable A₁ B₁] :
Algebra.IsSeparable A₂ B₂
source
theorem AlgHom.natCard_of_powerBasis {S : Type u_2} [CommRing S] {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K S] [Algebra K L] (pb : PowerBasis K S) (h_sep : IsSeparable K pb.gen) (h_splits : Polynomial.Splits (algebraMap K L) (minpoly K pb.gen)) :
Nat.card (S →ₐ[K] L) = pb.dim
source
theorem AlgHom.card_of_powerBasis {S : Type u_2} [CommRing S] {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K S] [Algebra K L] (pb : PowerBasis K S) (h_sep : IsSeparable K pb.gen) (h_splits : Polynomial.Splits (algebraMap K L) (minpoly K pb.gen)) :
Fintype.card (S →ₐ[K] L) = pb.dim