finiteExts — Mathlib

English

For a field extension L/K,finiteExts K L is the set of intermediate fields E with E/K finite dimensional.

Русский

Для расширения полей L/K множество finiteExts K L состоит из промежуточных полей E, для которых E/K конечномерно.

LaTeX

$$$finiteExts\\ (K,L) = \\{ E: IntermediateField\ n_K_L \mid \\dim_K E < \\infty\\}$$$

Lean4

/-- Given a field extension `L/K`, `finiteExts K L` is the set of
intermediate field extensions `L/E/K` such that `E/K` is finite. -/
def finiteExts (K : Type*) [Field K] (L : Type*) [Field L] [Algebra K L] : Set (IntermediateField K L) :=
  {E | FiniteDimensional K E}

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