insepDegree — Mathlib

English

The (infinite) inseparable degree of E over F is the rank of E over SeparableClosure F E.

Русский

Несепарабельная степень E над F равна рангу E как модуля над сепарабельным замыканием SeparableClosure(F,E).

LaTeX

$$$\\mathrm{insepDegree}(F,E) = \\operatorname{rank}_{\\mathrm{separableClosure}(F,E)} E$$$

Lean4

/-- The (infinite) inseparable degree for a general field extension `E / F` is defined
to be the degree of `E / separableClosure F E`. -/
@[stacks 030L "Part 2"]
def insepDegree :=
  Module.rank (separableClosure F E) E

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