English
For α ∈ E algebraic over F, the separable degree of F⟮α⟯/F equals the natSepDegree of minpoly F α.
Русский
Пусть α ∈ E алгебраически над F. Тогда степен сепарабельности F⟮α⟯/F равна natSepDegree(minpoly F α).
LaTeX
$$$ finSepDegree F F\⟮α⟯ = (minpoly F α).natSepDegree $$$
Lean4
/-- The separable degree of `F⟮α⟯ / F` is equal to the separable degree of the
minimal polynomial of `α` over `F`. -/
theorem finSepDegree_adjoin_simple_eq_natSepDegree {α : E} (halg : IsAlgebraic F α) :
finSepDegree F F⟮α⟯ = (minpoly F α).natSepDegree :=
by
have : finSepDegree F F⟮α⟯ = _ :=
Nat.card_congr (algHomAdjoinIntegralEquiv F (K := AlgebraicClosure F⟮α⟯) halg.isIntegral)
classical
rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯), ← Fintype.card_coe]
simp_rw [Multiset.mem_toFinset]
-- The separable degree of `F⟮α⟯ / F` divides the degree of `F⟮α⟯ / F`.
-- Marked as `private` because it is a special case of `finSepDegree_dvd_finrank`.
