zero_seq

Mathlib.GroupTheory.FreeAbelianGroup

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

English

Pure distributes through applicative: pure f <*> x = f <$> x.

Русский

Чистая функция распределяется через аппликатив: pure f <*> x = f <$> x.

LaTeX

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

Lean4

@[simp]
theorem zero_seq (x : FreeAbelianGroup α) : (0 : FreeAbelianGroup (α → β)) <*> x = 0 :=
  zero_bind _

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

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

Разделы

Аффилиация

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