chore: Move MulAction to under Algebra (#13140)

Move the content of `GroupTheory.GroupAction.Defs` that doesn't depend on `GroupWithZero` to a new file `Algebra.Group.Action.Defs`. This is part of #13027.
leanprover-community · May 24, 2024 · 7476a96 · 7476a96
1 parent 4b398c7
commit 7476a96
Show file tree

Hide file tree

Showing 11 changed files with 847 additions and 877 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -185,6 +185,7 @@ import Mathlib.Algebra.GCDMonoid.Nat
 import Mathlib.Algebra.GeomSum
 import Mathlib.Algebra.GradedMonoid
 import Mathlib.Algebra.GradedMulAction
+import Mathlib.Algebra.Group.Action.Defs
 import Mathlib.Algebra.Group.AddChar
 import Mathlib.Algebra.Group.Aut
 import Mathlib.Algebra.Group.Basic

diff --git a/Mathlib/Algebra/FreeMonoid/Basic.lean b/Mathlib/Algebra/FreeMonoid/Basic.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.Group.List
+import Mathlib.Algebra.Group.Action.Defs
 import Mathlib.Algebra.Group.Units
-import Mathlib.GroupTheory.GroupAction.Defs
 
 #align_import algebra.free_monoid.basic from "leanprover-community/mathlib"@"657df4339ae6ceada048c8a2980fb10e393143ec"
 

diff --git a/Mathlib/Algebra/GradedMonoid.lean b/Mathlib/Algebra/GradedMonoid.lean
@@ -6,7 +6,7 @@ Authors: Eric Wieser
 import Mathlib.Algebra.BigOperators.Group.List
 import Mathlib.Algebra.Group.InjSurj
 import Mathlib.Data.List.FinRange
-import Mathlib.GroupTheory.GroupAction.Defs
+import Mathlib.Algebra.Group.Action.Defs
 import Mathlib.Data.SetLike.Basic
 import Mathlib.Algebra.Group.Submonoid.Basic
 import Mathlib.Data.Sigma.Basic

diff --git a/Mathlib/Algebra/Group/Action/Defs.lean b/Mathlib/Algebra/Group/Action/Defs.lean
diff --git a/Mathlib/CategoryTheory/Endomorphism.lean b/Mathlib/CategoryTheory/Endomorphism.lean
@@ -3,12 +3,12 @@ Copyright (c) 2019 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Scott Morrison, Simon Hudon
 -/
+import Mathlib.Algebra.Group.Action.Defs
 import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.Algebra.Group.Units
 import Mathlib.Algebra.Group.Units.Hom
 import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.Opposites
-import Mathlib.GroupTheory.GroupAction.Defs
 
 #align_import category_theory.endomorphism from "leanprover-community/mathlib"@"32253a1a1071173b33dc7d6a218cf722c6feb514"
 

diff --git a/Mathlib/GroupTheory/GroupAction/Defs.lean b/Mathlib/GroupTheory/GroupAction/Defs.lean
diff --git a/Mathlib/GroupTheory/GroupAction/Group.lean b/Mathlib/GroupTheory/GroupAction/Group.lean
@@ -22,14 +22,6 @@ universe u v w
 variable {α : Type u} {β : Type v} {γ : Type w}
 
 section MulAction
-
-/-- `Monoid.toMulAction` is faithful on cancellative monoids. -/
-@[to_additive " `AddMonoid.toAddAction` is faithful on additive cancellative monoids. "]
-instance RightCancelMonoid.faithfulSMul [RightCancelMonoid α] : FaithfulSMul α α :=
-  ⟨fun h => mul_right_cancel (h 1)⟩
-#align right_cancel_monoid.to_has_faithful_smul RightCancelMonoid.faithfulSMul
-#align add_right_cancel_monoid.to_has_faithful_vadd AddRightCancelMonoid.faithfulVAdd
-
 section Group
 
 variable [Group α] [MulAction α β]

diff --git a/Mathlib/GroupTheory/GroupAction/Option.lean b/Mathlib/GroupTheory/GroupAction/Option.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.GroupTheory.GroupAction.Defs
+import Mathlib.Algebra.Group.Action.Defs
 
 #align_import group_theory.group_action.option from "leanprover-community/mathlib"@"f1a2caaf51ef593799107fe9a8d5e411599f3996"
 

diff --git a/Mathlib/GroupTheory/GroupAction/Ring.lean b/Mathlib/GroupTheory/GroupAction/Ring.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
+import Mathlib.Algebra.Group.Action.Defs
 import Mathlib.Algebra.Ring.Defs
-import Mathlib.GroupTheory.GroupAction.Defs
 
 /-!
 # Commutativity and associativity of action of integers on rings

diff --git a/Mathlib/GroupTheory/GroupAction/Sigma.lean b/Mathlib/GroupTheory/GroupAction/Sigma.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.GroupTheory.GroupAction.Defs
+import Mathlib.Algebra.Group.Action.Defs
 
 #align_import group_theory.group_action.sigma from "leanprover-community/mathlib"@"f1a2caaf51ef593799107fe9a8d5e411599f3996"
 

diff --git a/Mathlib/GroupTheory/GroupAction/Sum.lean b/Mathlib/GroupTheory/GroupAction/Sum.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.GroupTheory.GroupAction.Defs
+import Mathlib.Algebra.Group.Action.Defs
 
 #align_import group_theory.group_action.sum from "leanprover-community/mathlib"@"f1a2caaf51ef593799107fe9a8d5e411599f3996"