finInsepDegree — Mathlib

English

The finite inseparable degree is the natural-number version of the inseparable degree; it is zero if the extension is infinite.

Русский

Конечная несепарабельная степень — это числовая (натуралная) версия несепарабельной степени; она равна нулю, если расширение бесконечно.

LaTeX

$$$\\mathrm{finInsepDegree}(F,E) = \\operatorname{finrank}(\\mathrm{separableClosure}(F,E), E)$$$

Lean4

/-- The finite inseparable degree for a general field extension `E / F` is defined
to be the degree of `E / separableClosure F E` as a natural number. It is defined to be zero
if such field extension is infinite. -/
def finInsepDegree : ℕ :=
  finrank (separableClosure F E) E

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