instAddCommSemigroup — Mathlib

English

If α is an additive commutative semigroup, then Holor α ds forms an AddCommSemigroup with pointwise addition.

Русский

Если α — коммутативная добавочная полугруппа, Holor α ds образует AddCommSemigroup при точечном сложении.

LaTeX

$$$\text{If } α\text{ is AddCommSemigroup, then }\mathrm{Holor}(α, ds)\text{ is AddCommSemigroup with } (x+y)(t)=x(t)+y(t).}$$$

Lean4

instance [AddCommSemigroup α] : AddCommSemigroup (Holor α ds) :=
  Pi.addCommSemigroup

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