finSepDegree_le_finrank — Mathlib

English

The separable degree of any field extension E/F divides its degree; equivalently finSepDegree F E ∣ finrank F E.

Русский

Разделительная степень любого расширения полей E/F делится на степень расширения; эквивалентно finSepDegree F E делится на finrank F E.

LaTeX

$$$ finSepDegree F E \mid finrank F E $$$

Lean4

/-- The separable degree of a finite extension `E / F` is smaller than the degree of `E / F`. -/
@[stacks 09HA "The inequality"]
theorem finSepDegree_le_finrank [FiniteDimensional F E] : finSepDegree F E ≤ finrank F E :=
  Nat.le_of_dvd finrank_pos <| finSepDegree_dvd_finrank F E

Похожие утверждения