commSemigroup — Mathlib

English

If α is a commutative semigroup, Set α is a commutative semigroup under pointwise multiplication.

Русский

Если α — коммутативная полугруппа, Set α образует коммутативную полугруппу под точечным умножением.

LaTeX

$$$$ S * T = T * S, \quad \text{for all } S,T \subseteq \alpha. $$$$

Lean4

/-- `Set α` is a `CommSemigroup` under pointwise operations if `α` is. -/
@[to_additive /-- `Set α` is an `AddCommSemigroup` under pointwise operations if `α` is. -/
    ]
protected def commSemigroup : CommSemigroup (Set α) :=
  { Set.semigroup with mul_comm := fun _ _ => image2_comm mul_comm }

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