instCommMonoid — Mathlib

English

If Y is CommMonoid, LocallyConstant X Y inherits a CommMonoid structure with pointwise operations.

Русский

Если Y — коммод-моной, LocallyConstant X Y наследует CommMonoid соточно по точкам.

LaTeX

$$$\forall f,g:\mathrm{LocallyConstant}(X,Y),\; f\cdot g = g\cdot f\text{ pointwise};\; 1_{\mathrm{LocConst}} = \text{const}_X(1_Y).$$$

Lean4

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

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