feat: port Algebra.Homology.ImageToKernel (#3459)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
leanprover-community · Apr 17, 2023 · 53b3537 · 53b3537
1 parent df69443
commit 53b3537
Show file tree

Hide file tree

Showing 3 changed files with 467 additions and 14 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -132,6 +132,7 @@ import Mathlib.Algebra.Hom.Ring
 import Mathlib.Algebra.Hom.Units
 import Mathlib.Algebra.Homology.ComplexShape
 import Mathlib.Algebra.Homology.HomologicalComplex
+import Mathlib.Algebra.Homology.ImageToKernel
 import Mathlib.Algebra.IndicatorFunction
 import Mathlib.Algebra.Invertible
 import Mathlib.Algebra.IsPrimePow