commMonoid — Mathlib

English

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

Русский

Если α коммутативный моноид, то Filter α — коммутативный моноид под точечным умножением.

LaTeX

$$$\text{Filter}(\alpha)$ is a CommMonoid when $\alpha$ is a CommMonoid.$$

Lean4

/-- `Filter α` is a `CommMonoid` under pointwise operations if `α` is. -/
@[to_additive /-- `Filter α` is an `AddCommMonoid` under pointwise operations if `α` is. -/
    ]
protected def commMonoid [CommMonoid α] : CommMonoid (Filter α) :=
  { Filter.mulOneClass, Filter.commSemigroup with }

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