Theorem CochainComplex.HomComplex.Cocycle.isKernel'_lift_apply_coe_eq_δ

Modification history

2026-10-02 13:31
Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
feat(Algebra/Homology): more API for Ext in linear categories (#44190) …
Added CochainComplex.HomComplex.Cocycle.isKernel'_lift_apply_coe_eq_δView on Github →