sepDegree — Mathlib

English

The (infinite) separable degree of E over F is defined as the dimension of separableClosure F E over F.

Русский

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

LaTeX

$$$\\mathrm{sepDegree}(F,E) = \\operatorname{rank}_F(\\mathrm{separableClosure}(F,E))$$$

Lean4

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

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