monoid — Mathlib

English

If α is a Monoid, then Filter α is a Monoid under pointwise multiplication.

Русский

Если α — моноид, то Filter α образует моноид под точечным умножением.

LaTeX

$$$\mathrm{Filter}(\alpha)$ is a Monoid when $\alpha$ is a Monoid.$$

Lean4

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

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