chore(Algebra/Group/Subgroup): split Lattice, Map, Ker from `Ba…

…sic.lean` (#19295) The file `Algebra/Group/Subgroup/Basic.lean` is very long. Following the design of the `Submodule` folder, split it into: * `Lattice.lean`: `CompleteLattice` instance, `Subgroup.closure` * `Map.lean`: `Subgroup.map`, `Subgroup.comap` * `Ker.lean`: `MonoidHom.ker`, `MonoidHom.range` and `MonoidHom.eqLocus`
leanprover-community · Nov 21, 2024 · e4a142c · e4a142c
1 parent 1d199de
commit e4a142c
Show file tree

Hide file tree

Showing 23 changed files with 1,623 additions and 1,421 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -298,6 +298,9 @@ import Mathlib.Algebra.Group.Subgroup.Actions
 import Mathlib.Algebra.Group.Subgroup.Basic
 import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Algebra.Group.Subgroup.Finite
+import Mathlib.Algebra.Group.Subgroup.Ker
+import Mathlib.Algebra.Group.Subgroup.Lattice
+import Mathlib.Algebra.Group.Subgroup.Map
 import Mathlib.Algebra.Group.Subgroup.MulOpposite
 import Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
 import Mathlib.Algebra.Group.Subgroup.Order