English
Let R be a ring and s ⊆ R. Then the subalgebra of R generated by s over the integers ℤ coincides with the subalgebra coming from the subring closure of s; i.e. adjoin ℤ s = subalgebraOfSubring (Subring.closure s).
Русский
Пусть R — кольцо и s ⊆ R. Тогда подалгебра, порожденная s над целыми ℤ, равна подалгебре, порожденной s как подкольцо, то есть adjoin ℤ s = subalgebraOfSubring (Subring.closure s).
LaTeX
$$$ \operatorname{adjoin}_{\mathbb{Z}}(s) = \operatorname{subalgebraOfSubring}(\operatorname{Subring.closure}(s)). $$$
Lean4
theorem adjoin_int {R : Type*} [Ring R] (s : Set R) : adjoin ℤ s = subalgebraOfSubring (Subring.closure s) :=
le_antisymm (adjoin_le Subring.subset_closure)
(Subring.closure_le.2 subset_adjoin : Subring.closure s ≤ (adjoin ℤ s).toSubring)
