adjoin_adjoin_of_tower — Mathlib

English

For a tower of algebras with R → S → A, adjoin of S of the adjoin R s equals adjoin of S s, i.e., adjoin S (adjoin R s) = adjoin S s.

Русский

Для башни алгебр R → S → A зондировать adjoin: adjoin S (adjoin R s) = adjoin S s.

LaTeX

$$$ adjoin S (adjoin R s) = adjoin S s $$$

Lean4

theorem adjoin_adjoin_of_tower (s : Set A) : adjoin S (adjoin R s : Set A) = adjoin S s :=
  by
  apply le_antisymm (adjoin_le _)
  · exact adjoin_mono subset_adjoin
  · rw [← Subalgebra.coe_restrictScalars R (S := S), SetLike.coe_subset_coe]
    exact adjoin_le subset_adjoin

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