English
If all elements of a set s commute with each other, then closure(s) is a commutative ring.
Русский
Если все элементы множества s коммутируют друг с другом, то closure(s) является коммутативным кольцом.
LaTeX
$$$\\big(\\forall x\\in s\\,\\forall y\\in s,\\ xy = yx\\big) \\Rightarrow \\mathrm{closure}(s)\\text{ is a commutative ring}$$$
Lean4
/-- If all elements of `s : Set A` commute pairwise, then `closure s` is a commutative ring. -/
abbrev closureCommRingOfComm {s : Set R} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : CommRing (closure s) :=
{ (closure s).toRing with
mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
have := closure_le_centralizer_centralizer s
Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
