English
If every pair of elements of s commute, then every pair of elements of adjoin_R s commute (the adjoin becomes a commutative semiring, embedded as a substructure).
Русский
Если любые два элемента из s commute, то любые два элемента из adjoin_R s commute (порождающее становится коммутативной полускольной структурой).
LaTeX
$$$\\bigl(\\forall a\\in s,\\forall b\\in s,\\ ab=ba\\bigr) \\Rightarrow \\operatorname{adjoin}_R s \\text{ is a commutative semiring}$$$
Lean4
/-- If all elements of `s : Set A` commute pairwise, then `adjoin s` is a commutative semiring. -/
abbrev adjoinCommSemiringOfComm {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : CommSemiring (adjoin R s) :=
{ (adjoin R s).toSemiring with
mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
have := adjoin_le_centralizer_centralizer R s
Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
