chore(Algebra/Group/Subgroup): split off Defs file (#18340)

This PR splits off the definition of `Subgroup` and the `Group` instance into a new `Defs` file. Doing so required also moving the `Semigroup` instance on `Subsemigroup` and `Monoid` on `Submonoid` to the respective `Defs` file. So we needed to add one extra import: `Algebra.Group.InjSurj`. The imports and contents of that file are light enough in my opinion to make it worth it.




Co-authored-by: Anne Baanen <[email protected]>

Mathlib.lean

@@ -289,6 +289,7 @@ import Mathlib.Algebra.Group.Semiconj.Defs
 import Mathlib.Algebra.Group.Semiconj.Units
 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.MulOpposite
 import Mathlib.Algebra.Group.Subgroup.Order

Mathlib/Algebra/GradedMonoid.lean

@@ -4,11 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.BigOperators.Group.List
-import Mathlib.Algebra.Group.InjSurj
+import Mathlib.Algebra.Group.Action.End
+import Mathlib.Algebra.Group.Submonoid.Defs
 import Mathlib.Data.List.FinRange
-import Mathlib.Algebra.Group.Action.Defs
 import Mathlib.Data.SetLike.Basic
-import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Data.Sigma.Basic
 import Lean.Elab.Tactic