monoid — Mathlib

English

Set α forms a Monoid under pointwise operations if α is a Monoid.

Русский

Множество α образует моноид под точечными операциями, если α является моноидом.

LaTeX

$$$$ Set \alpha \text{ is a Monoid under pointwise operations if } \alpha \text{ is a Monoid}. $$$$

Lean4

/-- `Set α` is a `Monoid` under pointwise operations if `α` is. -/
@[to_additive /-- `Set α` is an `AddMonoid` under pointwise operations if `α` is. -/
    ]
protected def monoid : Monoid (Set α) :=
  { Set.semigroup, Set.mulOneClass, @Set.NPow α _ _ with }

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