English
The finite (Nat) rank of Subfield A ⊓ B over B equals the natural value of the cardinal rank: relfinrank A B = toNat (relrank A B).
Русский
Конечная (натуральная) ранк Subfield A ⊓ B над B равна натуральному значения кардинала relrank A B: relfinrank A B = toNat (relrank A B).
LaTeX
$$$\\mathrm{relfinrank}\\,A\\,B = \\operatorname{toNat}(\\mathrm{relrank}\\,A\\,B)$$$
Lean4
/-- `Subfield.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 :=
Module.rank ↥(A ⊓ B) (extendScalars (inf_le_right : A ⊓ B ≤ B))
