ofHom_sub

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

English

The cochain construction is additive with subtraction: ofHom(φ1 − φ2) = ofHom φ1 − ofHom φ2.

Русский

Сохранение вычитания: ofHom(φ1 − φ2) = ofHom(φ1) − ofHom(φ2).

LaTeX

$$$$\mathrm{ofHom}(\varphi_1 - \varphi_2) = \mathrm{ofHom}(\varphi_1) - \mathrm{ofHom}(\varphi_2).$$$$

Lean4

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

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

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

Разделы

Аффилиация

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