semigroup — Mathlib

English

If α is a semigroup, then Finset α is a semigroup under the pointwise product, defined by s · t = {xy : x ∈ s, y ∈ t}.

Русский

Если α — полугруппа, то Finset α образует полугруппу при точечном умножении: s·t = {xy : x∈s, y∈t}.

LaTeX

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

Lean4

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

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