seq_zero

Mathlib.GroupTheory.FreeAbelianGroup

URI: https://scilib.ai/kg/mathlib#FreeAbelianGroup.seq_zero

English

The product of any f with zero is zero: f <*> 0 = 0.

Русский

Произведение любого f с нулём равно нулю: f <*> 0 = 0.

LaTeX

$$$ \forall {\alpha \beta} (f : FreeAbelianGroup(\alpha \to \beta)),\; f <*> 0 = 0$$$

Lean4

@[simp]
theorem seq_zero (f : FreeAbelianGroup (α → β)) : f <*> 0 = 0 :=
  (seqAddGroupHom f).map_zero

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

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

Разделы

Аффилиация

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