monoid — Mathlib

English

If α is a monoid, then Finset α forms a monoid under the pointwise multiplication defined by s·t = {xy | x∈s, y∈t}, with the unit {1}.

Русский

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

LaTeX

$$$\\text{Finset}(\\alpha)$ is a Monoid with multiplication $s \\cdot t = \\{xy : x \\in s, y \\in t\\}$ and unit $\\{1\\}$.$$

Lean4

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

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