commMonoid — Mathlib

English

If α is a commutative monoid, then Finset α, with pointwise multiplication, forms a commutative monoid.

Русский

Если α — коммутативный моноид, то Finset α с точечным умножением образует коммутативный моноид.

LaTeX

$$Finset commMonoid: if α is a CommMonoid, then Finset α is a CommMonoid under pointwise operations.$$

Lean4

/-- `Finset α` is a `CommMonoid` under pointwise operations if `α` is. -/
@[to_additive /-- `Finset α` is an `AddCommMonoid` under pointwise operations if `α` is. -/
    ]
protected def commMonoid : CommMonoid (Finset α) :=
  coe_injective.commMonoid _ coe_one coe_mul coe_pow

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