English
For finite-dimensional E/F, finSepDegree F E = finrank F E if and only if E/F is separable.
Русский
Для конечномерного (финитного) расширения E/F верно: finSepDegree F E = finrank F E тогда и только тогда, когда E/F сепарабельно.
LaTeX
$$$ finSepDegree F E = finrank F E \iff Algebra.IsSeparable F E $$$
Lean4
/-- If `E / F` is a finite extension, then its separable degree is equal to its degree if and
only if it is a separable extension. -/
@[stacks 09HA "The equality condition"]
theorem finSepDegree_eq_finrank_iff [FiniteDimensional F E] :
finSepDegree F E = finrank F E ↔ Algebra.IsSeparable F E :=
⟨fun heq ↦
⟨fun x ↦ by
have halg := IsAlgebraic.of_finite F x
refine
(finSepDegree_adjoin_simple_eq_finrank_iff F E x halg).1 <|
le_antisymm (finSepDegree_adjoin_simple_le_finrank F E x halg) <| le_of_not_gt fun h ↦ ?_
have := Nat.mul_lt_mul_of_lt_of_le' h (finSepDegree_le_finrank F⟮x⟯ E) Fin.pos'
rw [finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E, Module.finrank_mul_finrank F F⟮x⟯ E] at this
linarith only [heq, this]⟩,
fun _ ↦ finSepDegree_eq_finrank_of_isSeparable F E⟩
