Theorems · Definition · field theory

IntermediateField.LinearDisjoint.basisOfBasisLeft

{F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {A B : IntermediateField F E} →
            A.LinearDisjoint ↥B →
              A.toSubalgebra ⊔ B.toSubalgebra = ⊤ → {ι : Type u_1} → Module.Basis ι F ↥A → Module.Basis ι (↥B) E

If A and B are linearly disjoint and such that A.toSubalgebra ⊔ B.toSubalgebra = ⊤, then any F-basis of A is also a B-basis of E. Note that the condition A.toSubalgebra ⊔ B.toSubalgebra = ⊤ is equivalent to A ⊔ B = ⊤ in many cases, see IntermediateField.sup_toSubalgebra_of_isAlgebraic_right and similar results.

Defined in

Mathlib.FieldTheory.LinearDisjoint

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra