Theorems · Definition · field theory

IntermediateField.LinearDisjoint

{F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          IntermediateField F E →
            (L : Type w) →
              [inst_3 : Field L] → [inst_4 : Algebra F L] → [inst_5 : Algebra L E] → [IsScalarTower F L E] → Prop

If A is an intermediate field of E / F, and E / L / F is a field extension tower, then A and L are linearly disjoint, if they are linearly disjoint as subalgebras of E (Subalgebra.LinearDisjoint).

Defined in

Mathlib.FieldTheory.LinearDisjoint

Cited by

82 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebraAlgebraIsScalarTower