seq_sub

Mathlib.GroupTheory.FreeAbelianGroup

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

← MathLib Explorer

English

A repeatable variant: f <*> x - y = (f <*> x) - (f <*> y).

Русский

Повторяемый вариант: f <*> x - y = (f <*> x) - (f <*> y).

LaTeX

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

Lean4

@[simp]
theorem seq_sub (f : FreeAbelianGroup (α → β)) (x y : FreeAbelianGroup α) : f <*> x - y = (f <*> x) - (f <*> y) :=
  (seqAddGroupHom f).map_sub x y

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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