feat: port Algebra.Module.Submodule.Lattice (#1898)

Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Jan 28, 2023 · 51f3caa · 51f3caa
1 parent b42511c
commit 51f3caa
Show file tree

Hide file tree

Showing 2 changed files with 425 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -95,6 +95,7 @@ import Mathlib.Algebra.Module.Pi
 import Mathlib.Algebra.Module.PointwisePi
 import Mathlib.Algebra.Module.Prod
 import Mathlib.Algebra.Module.Submodule.Basic
+import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.Algebra.Module.ULift
 import Mathlib.Algebra.NeZero
 import Mathlib.Algebra.Opposites