chore(group_theory/group_action/*): generalisation linter (#13100)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/group_theory/group_action/basic.lean

@@ -103,6 +103,20 @@ def stabilizer.submonoid (b : β) : submonoid α :=
   orbit α x = set.univ :=
 (surjective_smul α x).range_eq
 
+variables {α} {β}
+
+@[to_additive] lemma mem_fixed_points_iff_card_orbit_eq_one {a : β}
+  [fintype (orbit α a)] : a ∈ fixed_points α β ↔ fintype.card (orbit α a) = 1 :=
+begin
+  rw [fintype.card_eq_one_iff, mem_fixed_points],
+  split,
+  { exact λ h, ⟨⟨a, mem_orbit_self _⟩, λ ⟨b, ⟨x, hx⟩⟩, subtype.eq $ by simp [h x, hx.symm]⟩ },
+  { assume h x,
+    rcases h with ⟨⟨z, hz⟩, hz₁⟩,
+    calc x • a = z : subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩)
+      ... = a : (subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm }
+end
+
 end mul_action
 
 namespace mul_action
@@ -142,18 +156,6 @@ instance (x : β) : is_pretransitive α (orbit α x) :=
    orbit α a = orbit α b ↔ a ∈ orbit α b:=
 ⟨λ h, h ▸ mem_orbit_self _, λ ⟨c, hc⟩, hc ▸ orbit_smul _ _⟩
 
-@[to_additive] lemma mem_fixed_points_iff_card_orbit_eq_one {a : β}
-  [fintype (orbit α a)] : a ∈ fixed_points α β ↔ fintype.card (orbit α a) = 1 :=
-begin
-  rw [fintype.card_eq_one_iff, mem_fixed_points],
-  split,
-  { exact λ h, ⟨⟨a, mem_orbit_self _⟩, λ ⟨b, ⟨x, hx⟩⟩, subtype.eq $ by simp [h x, hx.symm]⟩ },
-  { assume h x,
-    rcases h with ⟨⟨z, hz⟩, hz₁⟩,
-    calc x • a = z : subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩)
-      ... = a : (subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm }
-end
-
 variables (α) {β}
 
 @[to_additive] lemma mem_orbit_smul (g : α) (a : β) : a ∈ orbit α (g • a) :=

src/group_theory/group_action/defs.lean

@@ -275,6 +275,35 @@ by exact {smul_comm := λ _ n, @smul_comm _ _ _ _ _ _ _ (g n) }
 
 end has_scalar
 
+section
+
+/-- Note that the `smul_comm_class α β β` typeclass argument is usually satisfied by `algebra α β`.
+-/
+@[to_additive]
+lemma mul_smul_comm [has_mul β] [has_scalar α β] [smul_comm_class α β β] (s : α) (x y : β) :
+  x * (s • y) = s • (x * y) :=
+(smul_comm s x y).symm
+
+/-- Note that the `is_scalar_tower α β β` typeclass argument is usually satisfied by `algebra α β`.
+-/
+lemma smul_mul_assoc [has_mul β] [has_scalar α β] [is_scalar_tower α β β] (r : α) (x y : β)  :
+  (r • x) * y = r • (x * y) :=
+smul_assoc r x y
+
+variables [has_scalar M α]
+
+lemma commute.smul_right [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α]
+  {a b : α} (h : commute a b) (r : M) :
+  commute a (r • b) :=
+(mul_smul_comm _ _ _).trans ((congr_arg _ h).trans $ (smul_mul_assoc _ _ _).symm)
+
+lemma commute.smul_left [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α]
+  {a b : α} (h : commute a b) (r : M) :
+  commute (r • a) b :=
+(h.symm.smul_right r).symm
+
+end
+
 section ite
 variables [has_scalar M α] (p : Prop) [decidable p]
 
@@ -363,36 +392,13 @@ instance is_scalar_tower.left : is_scalar_tower M M α :=
 
 variables {M}
 
-/-- Note that the `smul_comm_class α β β` typeclass argument is usually satisfied by `algebra α β`.
--/
-@[to_additive]
-lemma mul_smul_comm [has_mul β] [has_scalar α β] [smul_comm_class α β β] (s : α) (x y : β) :
-  x * (s • y) = s • (x * y) :=
-(smul_comm s x y).symm
-
-/-- Note that the `is_scalar_tower α β β` typeclass argument is usually satisfied by `algebra α β`.
--/
-lemma smul_mul_assoc [has_mul β] [has_scalar α β] [is_scalar_tower α β β] (r : α) (x y : β)  :
-  (r • x) * y = r • (x * y) :=
-smul_assoc r x y
-
 /-- Note that the `is_scalar_tower M α α` and `smul_comm_class M α α` typeclass arguments are
 usually satisfied by `algebra M α`. -/
 lemma smul_mul_smul [has_mul α] (r s : M) (x y : α)
   [is_scalar_tower M α α] [smul_comm_class M α α] :
   (r • x) * (s • y) = (r * s) • (x * y) :=
 by rw [smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
 
-lemma commute.smul_right [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α]
-  {a b : α} (h : commute a b) (r : M) :
-  commute a (r • b) :=
-(mul_smul_comm _ _ _).trans ((congr_arg _ h).trans $ (smul_mul_assoc _ _ _).symm)
-
-lemma commute.smul_left [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α]
-  {a b : α} (h : commute a b) (r : M) :
-  commute (r • a) b :=
-(h.symm.smul_right r).symm
-
 end
 
 namespace mul_action
@@ -444,8 +450,8 @@ by rw [smul_assoc, one_smul]
   (y : N) : (x • 1) * y = x • y :=
 smul_one_smul N x y
 
-@[simp, to_additive] lemma mul_smul_one {M N} [monoid N] [has_scalar M N] [smul_comm_class M N N]
-  (x : M) (y : N) :
+@[simp, to_additive] lemma mul_smul_one
+  {M N} [mul_one_class N] [has_scalar M N] [smul_comm_class M N N] (x : M) (y : N) :
   y * (x • 1) = x • y :=
 by rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]
 

src/group_theory/group_action/opposite.lean

@@ -106,12 +106,12 @@ instance comm_semigroup.is_central_scalar [comm_semigroup α] : is_central_scala
   one_smul := mul_one,
   mul_smul := λ x y r, (mul_assoc _ _ _).symm }
 
-instance is_scalar_tower.opposite_mid {M N} [monoid N] [has_scalar M N]
+instance is_scalar_tower.opposite_mid {M N} [has_mul N] [has_scalar M N]
   [smul_comm_class M N N] :
   is_scalar_tower M Nᵐᵒᵖ N :=
 ⟨λ x y z, mul_smul_comm _ _ _⟩
 
-instance smul_comm_class.opposite_mid {M N} [monoid N] [has_scalar M N]
+instance smul_comm_class.opposite_mid {M N} [has_mul N] [has_scalar M N]
   [is_scalar_tower M N N] :
   smul_comm_class M Nᵐᵒᵖ N :=
 ⟨λ x y z, by { induction y using mul_opposite.rec, simp [smul_mul_assoc] }⟩

src/group_theory/group_action/prod.lean

@@ -59,12 +59,12 @@ instance has_faithful_scalar_right [nonempty α] [has_faithful_scalar M β] :
 end
 
 @[to_additive]
-instance smul_comm_class_both [monoid N] [monoid P] [has_scalar M N] [has_scalar M P]
+instance smul_comm_class_both [has_mul N] [has_mul P] [has_scalar M N] [has_scalar M P]
   [smul_comm_class M N N] [smul_comm_class M P P] :
   smul_comm_class M (N × P) (N × P) :=
 ⟨λ c x y, by simp [smul_def, mul_def, mul_smul_comm]⟩
 
-instance is_scalar_tower_both [monoid N] [monoid P] [has_scalar M N] [has_scalar M P]
+instance is_scalar_tower_both [has_mul N] [has_mul P] [has_scalar M N] [has_scalar M P]
   [is_scalar_tower M N N] [is_scalar_tower M P P] :
   is_scalar_tower M (N × P) (N × P) :=
 ⟨λ c x y, by simp [smul_def, mul_def, smul_mul_assoc]⟩

src/group_theory/group_action/sub_mul_action.lean

@@ -219,7 +219,7 @@ end sub_mul_action
 
 namespace sub_mul_action
 
-variables [division_ring S] [semiring R] [mul_action R M]
+variables [group_with_zero S] [monoid R] [mul_action R M]
 variables [has_scalar S R] [mul_action S M] [is_scalar_tower S R M]
 variables (p : sub_mul_action R M) {s : S} {x y : M}