Theorems · Theorem · field theory

IntermediateField.sup_toSubalgebra_of_isAlgebraic

∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (E1 E2 : IntermediateField K L),
  Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2 → (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

The compositum of two intermediate fields is equal to the compositum of them as subalgebras, if one of them is algebraic over the base field.

Defined in

Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra