chore(GroupTheory/GroupAction): split off Defs file (#18345)

The goal of this PR is to have a file with the definitions for the orbit and stabilizer of a group, and enough theory to define quotient groups.

Author: Vierkantor

Mathlib.lean

@@ -2951,6 +2951,7 @@ import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.GroupTheory.GroupAction.Blocks
 import Mathlib.GroupTheory.GroupAction.CardCommute
 import Mathlib.GroupTheory.GroupAction.ConjAct
+import Mathlib.GroupTheory.GroupAction.Defs
 import Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
 import Mathlib.GroupTheory.GroupAction.DomAct.Basic
 import Mathlib.GroupTheory.GroupAction.Embedding

Mathlib/Algebra/Module/Submodule/Basic.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Field.Defs
+import Mathlib.Algebra.Group.Subgroup.Basic
 import Mathlib.Algebra.Group.Submonoid.Membership
+import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 import Mathlib.GroupTheory.GroupAction.SubMulAction
 
 /-!

Mathlib/CategoryTheory/Galois/GaloisObjects.lean

@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Galois.Basic
 import Mathlib.CategoryTheory.Limits.FintypeCat
 import Mathlib.CategoryTheory.Limits.Preserves.Limits
 import Mathlib.CategoryTheory.Limits.Shapes.SingleObj
+import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.Logic.Equiv.TransferInstance
 
 /-!

Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean

@@ -5,7 +5,8 @@ Authors: Christian Merten
 -/
 import Mathlib.CategoryTheory.Limits.Types
 import Mathlib.CategoryTheory.SingleObj
-import Mathlib.GroupTheory.GroupAction.Basic
+import Mathlib.Data.Setoid.Basic
+import Mathlib.GroupTheory.GroupAction.Defs
 
 /-!
 # (Co)limits of functors out of `SingleObj M`

Mathlib/Dynamics/Minimal.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.Topology.Algebra.ConstMulAction
 
 /-!

Mathlib/GroupTheory/Coset/Basic.lean

@@ -3,9 +3,12 @@ Copyright (c) 2018 Mitchell Rowett. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mitchell Rowett, Kim Morrison
 -/
-import Mathlib.Algebra.Quotient
 import Mathlib.Algebra.Group.Subgroup.MulOpposite
-import Mathlib.GroupTheory.GroupAction.Basic
+import Mathlib.Algebra.Quotient
+import Mathlib.Data.Fintype.Card
+import Mathlib.Data.Set.Pointwise.SMul
+import Mathlib.Data.Setoid.Basic
+import Mathlib.GroupTheory.GroupAction.Defs
 
 /-!
 # Cosets