commSemigroup — Mathlib

English

If α is a commutative semigroup, then Filter α is a commutative semigroup under pointwise multiplication; f * g = g * f.

Русский

Если α — коммутативная полугруппа, то Filter α образует коммутативную полугруппу под точечным умножением; f * g = g * f.

LaTeX

$$$\forall f,g \in \mathrm{Filter}(\alpha),\ f * g = g * f.$$$

Lean4

/-- `Filter α` is a `CommSemigroup` under pointwise operations if `α` is. -/
@[to_additive /-- `Filter α` is an `AddCommSemigroup` under pointwise operations if `α` is. -/
    ]
protected def commSemigroup [CommSemigroup α] : CommSemigroup (Filter α) :=
  { Filter.semigroup with mul_comm := fun _ _ => map₂_comm mul_comm }

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