Theorems · Definition · field theory

IntermediateField.relrank

{F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] → [inst_2 : Algebra F E] → IntermediateField F E → IntermediateField F E → Cardinal.{v}

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.

Defined in

Mathlib.FieldTheory.Relrank

Cited by

45 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra