Theorems · Definition · field theory

Subfield.relrank

{E : Type v} → [inst : Field E] → Subfield E → Subfield E → Cardinal.{v}

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.

Defined in

Mathlib.FieldTheory.Relrank

Cited by

40 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Field