map_add

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.HomComplex.Cochain.map_add

English

Mapping respects addition: the image of a sum is the sum of the images.

Русский

Отображение сохраняет сложение: образ суммы равен сумме образов.

LaTeX

$$$\\big( z + z' \\big).map \\Phi = z.map \\Phi + z'.map \\Phi.$$$

Lean4

@[simp]
protected theorem map_add : (z + z').map Φ = z.map Φ + z'.map Φ := by cat_disch

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

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

Разделы

Аффилиация

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