chore(algebra/group_power/lemmas): turn [zn]smul lemmas into instances (#13002)

This adds new instances such that:

* `mul_[zn]smul_assoc` is `←smul_mul_assoc`
* `mul_[zn]smul_left` is `←mul_smul_comm`

This also makes `noncomm_ring` slightly smarter, and able to handle scalar actions by `nat`.
Thanks to Christopher, this generalizes these instances to non-associative and non-unital rings.

Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>

Author: eric-wieser

src/algebra/group_power/lemmas.lean

@@ -342,11 +342,21 @@ by induction n with n ih; [rw [zero_nsmul, nat.cast_zero, mul_zero],
 @[simp] theorem nsmul_eq_mul [semiring R] (n : ℕ) (a : R) : n • a = n * a :=
 by rw [nsmul_eq_mul', (n.cast_commute a).eq]
 
-theorem mul_nsmul_left [semiring R] (a b : R) (n : ℕ) : n • (a * b) = a * (n • b) :=
-by rw [nsmul_eq_mul', nsmul_eq_mul', mul_assoc]
-
-theorem mul_nsmul_assoc [semiring R] (a b : R) (n : ℕ) : n • (a * b) = n • a * b :=
-by rw [nsmul_eq_mul, nsmul_eq_mul, mul_assoc]
+/-- Note that `add_comm_monoid.nat_smul_comm_class` requires stronger assumptions on `R`. -/
+instance non_unital_non_assoc_semiring.nat_smul_comm_class [non_unital_non_assoc_semiring R] :
+  smul_comm_class ℕ R R :=
+⟨λ n x y, match n with
+  | 0 := by simp_rw [zero_nsmul, smul_eq_mul, mul_zero]
+  | (n + 1) := by simp_rw [succ_nsmul, smul_eq_mul, mul_add, ←smul_eq_mul, _match n]
+  end⟩
+
+/-- Note that `add_comm_monoid.nat_is_scalar_tower` requires stronger assumptions on `R`. -/
+instance non_unital_non_assoc_semiring.nat_is_scalar_tower [non_unital_non_assoc_semiring R] :
+  is_scalar_tower ℕ R R :=
+⟨λ n x y, match n with
+  | 0 := by simp_rw [zero_nsmul, smul_eq_mul, zero_mul]
+  | (n + 1) := by simp_rw [succ_nsmul, ←_match n, smul_eq_mul, add_mul]
+  end⟩
 
 @[simp, norm_cast] theorem nat.cast_pow [semiring R] (n m : ℕ) : (↑(n ^ m) : R) = ↑n ^ m :=
 begin
@@ -383,11 +393,21 @@ by { dsimp [bit1], rw [mul_add, mul_bit0, mul_one], }
 theorem zsmul_eq_mul' [ring R] (a : R) (n : ℤ) : n • a = a * n :=
 by rw [zsmul_eq_mul, (n.cast_commute a).eq]
 
-theorem mul_zsmul_left [ring R] (a b : R) (n : ℤ) : n • (a * b) = a * (n • b) :=
-by rw [zsmul_eq_mul', zsmul_eq_mul', mul_assoc]
-
-theorem mul_zsmul_assoc [ring R] (a b : R) (n : ℤ) : n • (a * b) = n • a * b :=
-by rw [zsmul_eq_mul, zsmul_eq_mul, mul_assoc]
+/-- Note that `add_comm_group.int_smul_comm_class` requires stronger assumptions on `R`. -/
+instance non_unital_non_assoc_ring.int_smul_comm_class [non_unital_non_assoc_ring R] :
+  smul_comm_class ℤ R R :=
+⟨λ n x y, match n with
+  | (n : ℕ) := by simp_rw [coe_nat_zsmul, smul_comm]
+  | -[1+n]  := by simp_rw [zsmul_neg_succ_of_nat, smul_eq_mul, mul_neg, mul_smul_comm]
+  end⟩
+
+/-- Note that `add_comm_group.int_is_scalar_tower` requires stronger assumptions on `R`. -/
+instance non_unital_non_assoc_ring.int_is_scalar_tower [non_unital_non_assoc_ring R] :
+  is_scalar_tower ℤ R R :=
+⟨λ n x y, match n with
+  | (n : ℕ) := by simp_rw [coe_nat_zsmul, smul_assoc]
+  | -[1+n]  := by simp_rw [zsmul_neg_succ_of_nat, smul_eq_mul, neg_mul, smul_mul_assoc]
+  end⟩
 
 lemma zsmul_int_int (a b : ℤ) : a • b = a * b := by simp
 

src/tactic/noncomm_ring.lean

@@ -26,7 +26,7 @@ meta def noncomm_ring :=
              -- Replace multiplication by numerals with `zsmul`.
              bit0_mul, mul_bit0, bit1_mul, mul_bit1, one_mul, mul_one, zero_mul, mul_zero,
              -- Pull `zsmul n` out the front so `abel` can see them.
-             ←mul_zsmul_assoc, ←mul_zsmul_left,
+             mul_smul_comm, smul_mul_assoc,
              -- Pull out negations.
              neg_mul, mul_neg] {fail_if_unchanged := ff};
   abel]

test/noncomm_ring.lean

@@ -22,6 +22,7 @@ example : a ^ 3 = a * a * a := by noncomm_ring
 example : (-a) * b = -(a * b) := by noncomm_ring
 example : a * (-b) = -(a * b) := by noncomm_ring
 example : a * (b + c + b + c - 2*b) = 2*a*c := by noncomm_ring
+example : a * (b + c + b + c - (2 : ℕ) • b) = 2*a*c := by noncomm_ring
 example : (a + b)^2 = a^2 + a*b + b*a + b^2 := by noncomm_ring
 example : (a - b)^2 = a^2 - a*b - b*a + b^2 := by noncomm_ring
 example : (a + b)^3 = a^3 + a^2*b + a*b*a + a*b^2 + b*a^2 + b*a*b + b^2*a + b^3 := by noncomm_ring