English
If all elements of s commute pairwise (and with star, in the star-case), then the adjoin R s forms a commutative ring.
Русский
Если элементы s взаимно коммутируют (и с сопряжением, в случае звезды), то адъюнкт R s образует коммутативное кольцо.
LaTeX
$$$\operatorname{CommRing}(\operatorname{adjoin}_R s).$$$
Lean4
/-- If all elements of `s : Set A` commute pairwise and also commute pairwise with elements of
`star s`, then `StarSubalgebra.adjoin R s` is commutative. See note [reducible non-instances]. -/
abbrev adjoinCommRingOfComm (R : Type u) {A : Type v} [CommRing R] [StarRing R] [Ring A] [Algebra R A] [StarRing A]
[StarModule R A] {s : Set A} (hcomm : ∀ a : A, a ∈ s → ∀ b : A, b ∈ s → a * b = b * a)
(hcomm_star : ∀ a : A, a ∈ s → ∀ b : A, b ∈ s → a * star b = star b * a) : CommRing (adjoin R s) :=
{ StarAlgebra.adjoinCommSemiringOfComm R hcomm hcomm_star, (adjoin R s).toSubalgebra.toRing with }
