Theorems · Theorem · field theory

IntermediateField.LinearDisjoint.of_finrank_sup

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

If A and B are finite extensions of F, such that rank of A ⊔ B is equal to the product of the rank of A and B, then A and B are linearly disjoint.

Defined in

Mathlib.FieldTheory.LinearDisjoint

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFiniteDimensionalFiniteDimensional