Theorems · Theorem · field theory

IntermediateField.LinearDisjoint.finrank_left_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 ↥A], A.LinearDisjoint ↥B → A ⊔ B = ⊤ → Module.finrank (↥A) E = Module.finrank F ↥B

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

Defined in

Mathlib.FieldTheory.LinearDisjoint

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraModule.Finite