map_neg

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

English

The map of the negation is the negation of the map: (−z).map Φ = −(z.map Φ).

Русский

Отображение отрицания равно отрицанию отображения: (−z).map Φ = −(z.map Φ).

LaTeX

$$$(-z).map\\;\\Phi = -\\big(z.map\\;\\Phi\\big).$$$

Lean4

@[simp]
protected theorem map_neg : (-z).map Φ = -z.map Φ := by cat_disch

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

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

Разделы

Аффилиация

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