Theorem ChainComplex.of_d_ne

Modification history

2026-04-30 19:12
Mathlib/Algebra/Homology/HomologicalComplex.lean
chore(Algebra/Homology/HomologicalComplex): make CochainComplex.of and ChainComplex.of abbrevs (#38661) …
Modified ChainComplex.of_d_neView on Github →
2023-04-17 19:17
Mathlib/Algebra/Homology/HomologicalComplex.lean
feat: port Algebra.Homology.HomologicalComplex (#3451)
Added ChainComplex.of_d_neView on Github →