map_zero — Mathlib

English

In the HomComplex, δ respects postcomposition with a morphism: δ(n,m)((Cochain.ofHom f).comp z) = (Cochain.ofHom f).comp (δ(n,m) z).

Русский

В HomComplex δ сохраняет пост-композицию с морфизмом: δ(n,m)((Cochain.ofHom f).comp z) = (Cochain.ofHom f).comp (δ(n,m) z).

LaTeX

$$$\\delta(n,m)((\\mathrm{Cochain.ofHom}(f) \\circ z)) = (\\mathrm{Cochain.ofHom}(f) \\circ (\\delta(n,m) z)).$$$

Lean4

@[simp]
protected theorem map_zero : (0 : Cochain K L n).map Φ = 0 := by cat_disch

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