sumAddHom_zero

Mathlib.Data.DFinsupp.BigOperators

URI: https://scilib.ai/kg/mathlib#DFinsupp.sumAddHom_zero

English

If every coordinate map is zero, sumAddHom is the zero map.

Русский

Если все координатные отображения равны нулю, сумма sumAddHom отображается как ноль.

LaTeX

$$$ \\operatorname{sumAddHom} \\bigl( \\lambda i. 0: β_i → γ \\bigr) = 0. $$$

Lean4

@[simp]
theorem sumAddHom_zero [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] : (sumAddHom fun i => (0 : β i →+ γ)) = 0 :=
  map_zero liftAddHom

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

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

Разделы

Аффилиация

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