Def ChainComplex.of.d

Modification history

2026-04-30 19:12

Mathlib/Algebra/Homology/HomologicalComplex.lean

chore(Algebra/Homology/HomologicalComplex): make CochainComplex.of and ChainComplex.of abbrevs (#38661) …

Added ChainComplex.of.d View on Github →