Commit 2026-08-11 16:58 ac478694

View on Github →

chore(Algebra/Homology): make HomologicalComplex.eval implicit_reducible (#42648)

Estimated changes

Modified Mathlib/Algebra/Homology/Additive.lean

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

modified def HomologicalComplex.dNatTrans

Modified Mathlib/CategoryTheory/GradedObject.lean