English
The separable degree of a finite extension E/F divides its degree: finSepDegree F E ∣ finrank F E.
Русский
Разделительная степень конечного расширения E/F делится на степень расширения E/F: finSepDegree F E делится на finrank F E.
LaTeX
$$$ finSepDegree F E \mid finrank F E $$$
Lean4
/-- The separable degree of any field extension `E / F` divides the degree of `E / F`. -/
theorem finSepDegree_dvd_finrank : finSepDegree F E ∣ finrank F E :=
by
by_cases hfd : FiniteDimensional F E
· rw [← finSepDegree_top F, ← finrank_top F E]
refine
induction_on_adjoin (fun K : IntermediateField F E ↦ finSepDegree F K ∣ finrank F K)
(by simp_rw [finSepDegree_bot, IntermediateField.finrank_bot, one_dvd]) (fun L x h ↦ ?_) ⊤
simp only at h ⊢
have hdvd := mul_dvd_mul h <| finSepDegree_adjoin_simple_dvd_finrank L E x
set M := L⟮x⟯
rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M, Module.finrank_mul_finrank F L M] at hdvd
rw [finrank_of_infinite_dimensional hfd]
exact dvd_zero _
