English
Let E/F be an algebraic field extension. Then the finite separable degree finSepDegree F E equals the natural number corresponding to the separable degree sepDegree F E; in particular finSepDegree F E = toNat(sepDegree F E).
Русский
Пусть E/F — алгебраическое расширение поля. Тогда конечная сепарабельная степень finSepDegree F E равна натуральному числу, соответствующему сепарабельной степени sepDegree F E; то есть finSepDegree F E = toNat(sepDegree F E).
LaTeX
$$$\operatorname{finSepDegree} F E = \operatorname{toNat}\bigl(\operatorname{sepDegree} F E\bigr)$$$
Lean4
/-- If `E / F` is algebraic, then the `Field.finSepDegree F E` is equal to `Field.sepDegree F E`
as a natural number. This means that the cardinality of `Field.Emb F E` and the degree of
`(separableClosure F E) / F` are both finite or infinite, and when they are finite, they
coincide. -/
@[stacks 09HJ "`sepDegree` is defined as the right-hand side of 09HJ"]
theorem finSepDegree_eq [Algebra.IsAlgebraic F E] : finSepDegree F E = Cardinal.toNat (sepDegree F E) :=
by
have h := finSepDegree_mul_finSepDegree_of_isAlgebraic F (separableClosure F E) E |>.symm
haveI := separableClosure.isSeparable F E
haveI := separableClosure.isPurelyInseparable F E
rwa [finSepDegree_eq_finrank_of_isSeparable F (separableClosure F E),
IsPurelyInseparable.finSepDegree_eq_one (separableClosure F E) E, mul_one] at h
