feat: port Algebra.Homology.Additive (#3517)

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
leanprover-community · Apr 19, 2023 · b1e0bf7 · b1e0bf7
1 parent aea85a2
commit b1e0bf7
Show file tree

Hide file tree

Showing 2 changed files with 453 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -131,6 +131,7 @@ import Mathlib.Algebra.Hom.Iterate
 import Mathlib.Algebra.Hom.NonUnitalAlg
 import Mathlib.Algebra.Hom.Ring
 import Mathlib.Algebra.Hom.Units
+import Mathlib.Algebra.Homology.Additive
 import Mathlib.Algebra.Homology.ComplexShape
 import Mathlib.Algebra.Homology.Exact
 import Mathlib.Algebra.Homology.Flip