Theorems · Theorem · field theory

IntermediateField.LinearDisjoint.of_inf_eq_bot

∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  [IsGalois F ↥A] [FiniteDimensional F ↥A] [FiniteDimensional F ↥B], A ⊓ B = ⊥ → A.LinearDisjoint ↥B

If A and B are finite extensions of F, with A/F Galois, such that A ⊓ B = F, then A and B are linearly disjoint over F.

Defined in

Mathlib.FieldTheory.LinearDisjoint

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsGaloisFiniteDimensionalFiniteDimensional