feat(Algebra/Group/InjSurj): port file (#707)

mathlib3 SHA: f69e8f317a18ab43f12cdcacaa1a3765eb512065 This was a very straightforward port. Co-authored-by: David Wärn <[email protected]>
leanprover-community · Nov 24, 2022 · b711a3b · b711a3b
1 parent c174706
commit b711a3b
Show file tree

Hide file tree

Showing 2 changed files with 457 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -5,6 +5,7 @@ import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Commutator
 import Mathlib.Algebra.Group.Commute
 import Mathlib.Algebra.Group.Defs
+import Mathlib.Algebra.Group.InjSurj
 import Mathlib.Algebra.Group.OrderSynonym
 import Mathlib.Algebra.Group.Semiconj
 import Mathlib.Algebra.Group.Units