sup_toSubalgebra_of_isAlgebraic_left

English

If E1 is algebraic over K, then the same equality as in the right-hand version holds with E1 and E2 swapped: (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra.

Русский

Если E1 алгебраическое над K, то равенство подалгебр сохраняется при перестановке E1 и E2.

LaTeX

$$$(E_1 \sqcup E_2)^{\text{toSubalgebra}} = E_1^{\text{toSubalgebra}} \sqcup E_2^{\text{toSubalgebra}}$$$

Lean4

theorem sup_toSubalgebra_of_isAlgebraic_left [Algebra.IsAlgebraic K E1] :
    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
  by
  have := sup_toSubalgebra_of_isAlgebraic_right E2 E1
  rwa [sup_comm (a := E1), sup_comm (a := E1.toSubalgebra)]

Похожие утверждения