feat: port Algebra.Module.Injective (#3873)

leanprover-community · May 11, 2023 · 791d8dd · 791d8dd
1 parent cc90075
commit 791d8dd
Show file tree

Hide file tree

Showing 2 changed files with 473 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -167,6 +167,7 @@ import Mathlib.Algebra.Module.Basic
 import Mathlib.Algebra.Module.BigOperators
 import Mathlib.Algebra.Module.Equiv
 import Mathlib.Algebra.Module.Hom
+import Mathlib.Algebra.Module.Injective
 import Mathlib.Algebra.Module.LinearMap
 import Mathlib.Algebra.Module.Opposites
 import Mathlib.Algebra.Module.Pi