instCommSemigroup — Mathlib

English

If Y is a commutative semigroup, LocallyConstant X Y inherits a commutative semigroup structure with (f*g)(x) = f(x) g(x).

Русский

Если Y — коммутативная полугруппа, LocallyConstant X Y наследует коммутативную полугруппу: (f*g)(x) = f(x) g(x).

LaTeX

$$$\forall f,g:\mathrm{LocallyConstant}(X,Y),\; (f*g)(x) = f(x)g(x) = g(x)f(x) = (g*f)(x).$$$

Lean4

@[to_additive]
instance [CommSemigroup Y] : CommSemigroup (LocallyConstant X Y) :=
  Function.Injective.commSemigroup DFunLike.coe DFunLike.coe_injective' fun _ _ => rfl

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