Theorems · Theorem · field theory

IntermediateField.LinearDisjoint.finrank_right_eq_finrank

∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  [Module.Finite F ↥B], A.LinearDisjoint ↥B → A ⊔ B = ⊤ → Module.finrank (↥B) E = Module.finrank F ↥A

If A and B are linearly disjoint over F and A ⊔ B = E, then the Module.finrank of E over B is equal to the Module.finrank of A over F.

Defined in

Mathlib.FieldTheory.LinearDisjoint

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraModule.Finite