ofHom_neg

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

English

Negation commutes with the ofHom construction: ofHom(−φ) = −(ofHom φ).

Русский

Негация и конструкция ofHom коммутируют: ofHom(−φ) = −(ofHom φ).

LaTeX

$$$$\mathrm{ofHom}(-\varphi) = -\mathrm{ofHom}(\varphi).$$$$

Lean4

@[simp]
theorem ofHom_neg (φ : F ⟶ G) : Cochain.ofHom (-φ) = -Cochain.ofHom φ := by cat_disch

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

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

Разделы

Аффилиация

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