English
For any field extension E/F, the finite separable degree times the finite inseparable degree equals the finite extension degree: finSepDegree F E · finInsepDegree F E = finrank F E.
Русский
Для любого полевого расширения E/F произведение конечной сепарабельной степени на конечную неразделимую степень равно конечной степени расширения: finSepDegree F E · finInsepDegree F E = finrank F E.
LaTeX
$$$\operatorname{finSepDegree} F E \cdot \operatorname{finInsepDegree} F E = \operatorname{finrank} F E$$$
Lean4
/-- The finite separable degree multiply by the finite inseparable degree is equal
to the (finite) field extension degree. -/
theorem finSepDegree_mul_finInsepDegree : finSepDegree F E * finInsepDegree F E = finrank F E :=
by
by_cases halg : Algebra.IsAlgebraic F E
· have := congr_arg Cardinal.toNat (sepDegree_mul_insepDegree F E)
rwa [Cardinal.toNat_mul, ← finSepDegree_eq F E] at this
rw [finInsepDegree,
finrank_of_infinite_dimensional (K := F) (V := E) fun _ ↦ halg (Algebra.IsAlgebraic.of_finite F E),
finrank_of_infinite_dimensional (K := separableClosure F E) (V := E) fun _ ↦
halg (.trans _ (separableClosure F E) _),
mul_zero]
