instAddCommMonoid — Mathlib

English

If α is an additive commutative monoid, then the holor α ds (the space of ds-indexed α-valued holors) forms an AddCommMonoid under pointwise addition.

Русский

Если α — коммутативный аддитивный моноид, то пространство Holor α ds (функторы с индексами ds) образует AddCommMonoid с покомпонентным сложением.

LaTeX

$$AddCommMonoid (Holor α ds)$$

Lean4

instance [AddCommMonoid α] : AddCommMonoid (Holor α ds) :=
  Pi.addCommMonoid

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