instAddMonoid

Mathlib.Data.Holor

URI: https://scilib.ai/kg/mathlib#Holor.instAddMonoid

English

If α is an AddMonoid, then Holor α ds forms an AddMonoid with pointwise addition.

Русский

Если α — AddMonoid, Holor α ds образует AddMonoid при точечном сложении.

LaTeX

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

Lean4

instance [AddMonoid α] : AddMonoid (Holor α ds) :=
  Pi.addMonoid

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru