commSemigroup — Mathlib

English

If α is a commutative semigroup, then Finset α is a commutative semigroup under the pointwise product.

Русский

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

LaTeX

$$$$ \\text{If } \\alpha \\text{ is a commutative semigroup, then Finset }\\alpha \\text{ is a commutative semigroup under pointwise product.} $$$$

Lean4

/-- `Finset α` is a `CommSemigroup` under pointwise operations if `α` is. -/
@[to_additive /-- `Finset α` is an `AddCommSemigroup` under pointwise operations if `α` is. -/
    ]
protected def commSemigroup : CommSemigroup (Finset α) :=
  coe_injective.commSemigroup _ coe_mul

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