commMonoid — Mathlib

English

If α is a commutative monoid, then Set α equipped with pointwise operations forms a commutative monoid.

Русский

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

LaTeX

$$$\text{If } \alpha \text{ is a commutative monoid, then } Set(\alpha) \text{ is a commutative monoid}$$$

Lean4

/-- `Set α` is a `CommMonoid` under pointwise operations if `α` is. -/
@[to_additive /-- `Set α` is an `AddCommMonoid` under pointwise operations if `α` is. -/
    ]
protected def commMonoid [CommMonoid α] : CommMonoid (Set α) :=
  { Set.monoid, Set.commSemigroup with }

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