chore: move Submodule.{map,comap} to Algebra.Module.Submodule.Map (#7925

)
leanprover-community · Oct 26, 2023 · 49f7f62 · 49f7f62
1 parent c6cb8b6
commit 49f7f62
Show file tree

Hide file tree

Showing 3 changed files with 623 additions and 557 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -311,6 +311,7 @@ import Mathlib.Algebra.Module.Projective
 import Mathlib.Algebra.Module.Submodule.Basic
 import Mathlib.Algebra.Module.Submodule.Bilinear
 import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Algebra.Module.Submodule.Map
 import Mathlib.Algebra.Module.Submodule.Pointwise
 import Mathlib.Algebra.Module.Torsion
 import Mathlib.Algebra.Module.ULift