feat: port Algebra.Category.GroupCat.EpiMono (#3871)

Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
leanprover-community · May 10, 2023 · 94759f8 · 94759f8
1 parent 5e04039
commit 94759f8
Show file tree

Hide file tree

Showing 2 changed files with 478 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -30,6 +30,7 @@ import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.BigOperators.RingEquiv
 import Mathlib.Algebra.Bounds
 import Mathlib.Algebra.Category.GroupCat.Basic
+import Mathlib.Algebra.Category.GroupCat.EpiMono
 import Mathlib.Algebra.Category.GroupCat.EquivalenceGroupAddGroup
 import Mathlib.Algebra.Category.GroupCat.Preadditive
 import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence