relrank — Mathlib

English

The relrank of intermediate field extensions is defined as the relrank of the corresponding subfields, i.e., relrank(A,B) = [B : A ∩ B].

Русский

Relrank промежуточного поля A над B определяется как [B : A ∩ B].

LaTeX

$$$\\operatorname{relrank}(A,B) = [B : A \\cap B].$$$

Lean4

/-- `IntermediateField.relrank A B` is defined to be `[B : A ⊓ B]` as a `Cardinal`, in particular,
when `A ≤ B` it is `[B : A]`, the degree of the field extension `B / A`.
This is similar to `Subgroup.relIndex` but it is `Cardinal` valued. -/
noncomputable def relrank :=
  A.toSubfield.relrank B.toSubfield

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