ofHom_add — Mathlib

English

The cochain construction is additive in the morphism argument: 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_add (φ₁ φ₂ : F ⟶ G) : Cochain.ofHom (φ₁ + φ₂) = Cochain.ofHom φ₁ + Cochain.ofHom φ₂ := by cat_disch

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