closureCommSemigroupOfComm — Mathlib

English

If all elements of s commute with each other, then closure(s) forms a commutative semigroup.

Русский

Если все элементы s commute между собой, то closure(s) образует коммутативную полугруппу.

LaTeX

$$$ closure(s) \\text{ is a } CommSemigroup $$$

Lean4

/-- If all the elements of a set `s` commute, then `closure s` is a commutative semigroup. -/
@[to_additive /-- If all the elements of a set `s` commute, then `closure s` forms an additive
          commutative semigroup. -/
    ]
abbrev closureCommSemigroupOfComm {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : CommSemigroup (closure s) :=
  { MulMemClass.toSemigroup (closure s) 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₂) }

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