feat: port Algebra.Module.Submodule.Basic (#1888)

Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Jan 27, 2023 · 2ee6978 · 2ee6978
1 parent df48ae6
commit 2ee6978
Show file tree

Hide file tree

Showing 3 changed files with 654 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -93,6 +93,7 @@ import Mathlib.Algebra.Module.Opposites
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Algebra.Module.PointwisePi
 import Mathlib.Algebra.Module.Prod
+import Mathlib.Algebra.Module.Submodule.Basic
 import Mathlib.Algebra.NeZero
 import Mathlib.Algebra.Opposites
 import Mathlib.Algebra.Order.AbsoluteValue