English
If at least one of E1 or E2 is algebraic over K, then the compositum's subalgebra equals the join of the subalgebras: (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra.
Русский
Если хотя бы одно из E1 или E2 алгебраическое над K, то подалгебра композиции равна объединению подалгебр.
LaTeX
$$$(E_1 \sqcup E_2)^{\text{toSubalgebra}} = E_1^{\text{toSubalgebra}} \sqcup E_2^{\text{toSubalgebra}} \quad\text{при } E_1 \text{ или } E_2 \text{ алгебраическое над } K$$$
Lean4
/-- 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. -/
theorem sup_toSubalgebra_of_isAlgebraic (halg : Algebra.IsAlgebraic K E1 ∨ Algebra.IsAlgebraic K E2) :
(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
halg.elim (fun _ ↦ sup_toSubalgebra_of_isAlgebraic_left E1 E2) (fun _ ↦ sup_toSubalgebra_of_isAlgebraic_right E1 E2)
