feat(group_theory/group_action/defs): add has_mul.to_has_scalar and…

… relax typeclass in `smul_mul_smul` (#7885)

src/data/matrix/basic.lean

@@ -508,8 +508,7 @@ by { ext, simp }
 by { ext, apply smul_dot_product }
 
 /-- This instance enables use with `smul_mul_assoc`. -/
-instance semiring.is_scalar_tower [decidable_eq n] [monoid R] [distrib_mul_action R α]
-  [is_scalar_tower R α α] :
+instance semiring.is_scalar_tower [monoid R] [distrib_mul_action R α] [is_scalar_tower R α α] :
   is_scalar_tower R (matrix n n α) (matrix n n α) :=
 ⟨λ r m n, matrix.smul_mul r m n⟩
 
@@ -518,8 +517,7 @@ instance semiring.is_scalar_tower [decidable_eq n] [monoid R] [distrib_mul_actio
 by { ext, apply dot_product_smul }
 
 /-- This instance enables use with `mul_smul_comm`. -/
-instance semiring.smul_comm_class [decidable_eq n] [monoid R] [distrib_mul_action R α]
-  [smul_comm_class R α α] :
+instance semiring.smul_comm_class [monoid R] [distrib_mul_action R α] [smul_comm_class R α α] :
   smul_comm_class R (matrix n n α) (matrix n n α) :=
 ⟨λ r m n, (matrix.mul_smul m r n).symm⟩
 

src/group_theory/group_action/defs.lean

@@ -55,6 +55,12 @@ class has_scalar (M : Type*) (α : Type*) := (smul : M → α → α)
 infix ` +ᵥ `:65 := has_vadd.vadd
 infixr ` • `:73 := has_scalar.smul
 
+/-- See also `monoid.to_mul_action` and `mul_zero_class.to_smul_with_zero`. -/
+@[priority 910, to_additive] -- see Note [lower instance priority]
+instance has_mul.to_has_scalar (α : Type*) [has_mul α] : has_scalar α α := ⟨(*)⟩
+
+@[simp, to_additive] lemma smul_eq_mul (α : Type*) [has_mul α] {a a' : α} : a • a' = a * a' := rfl
+
 /-- Type class for additive monoid actions. -/
 @[protect_proj] class add_action (G : Type*) (P : Type*) [add_monoid G] extends has_vadd G P :=
 (zero_vadd : ∀ p : P, (0 : G) +ᵥ p = p)
@@ -181,8 +187,6 @@ instance monoid.to_mul_action : mul_action M M :=
 This is promoted to an `add_torsor` by `add_group_is_add_torsor`. -/
 add_decl_doc add_monoid.to_add_action
 
-@[simp, to_additive] lemma smul_eq_mul {a a' : M} : a • a' = a * a' := rfl
-
 instance is_scalar_tower.left : is_scalar_tower M M α :=
 ⟨λ x y z, mul_smul x y z⟩
 
@@ -191,21 +195,22 @@ variables {M}
 /-- Note that the `smul_comm_class M α α` typeclass argument is usually satisfied by `algebra M α`.
 -/
 @[to_additive]
-lemma mul_smul_comm [monoid α] (s : M) (x y : α) [smul_comm_class M α α] :
+lemma mul_smul_comm [has_mul α] (s : M) (x y : α) [smul_comm_class M α α] :
   x * (s • y) = s • (x * y) :=
 (smul_comm s x y).symm
 
 /-- Note that the `is_scalar_tower M α α` typeclass argument is usually satisfied by `algebra M α`.
 -/
-lemma smul_mul_assoc [monoid α] (r : M) (x y : α) [is_scalar_tower M α α] :
+lemma smul_mul_assoc [has_mul α] (r : M) (x y : α) [is_scalar_tower M α α] :
   (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 [monoid α] (r s : M) (x y : α) [is_scalar_tower M α α] [smul_comm_class 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_smul]
+by rw [smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
 
 end