feat(algebra/*/basic): add trivial lemmas (#13416)

These save you from having to fiddle with `mul_one` when you want to rewrite them the other way, or allow easier commutativity rewrites.



Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

src/algebra/group/basic.lean

@@ -104,6 +104,14 @@ right_comm has_mul.mul mul_comm mul_assoc
 theorem mul_mul_mul_comm (a b c d : G) : (a * b) * (c * d) = (a * c) * (b * d) :=
 by simp only [mul_left_comm, mul_assoc]
 
+@[to_additive]
+lemma mul_rotate (a b c : G) : a * b * c = b * c * a :=
+by simp only [mul_left_comm, mul_comm]
+
+@[to_additive]
+lemma mul_rotate' (a b c : G) : a * (b * c) = b * (c * a) :=
+by simp only [mul_left_comm, mul_comm]
+
 end comm_semigroup
 
 local attribute [simp] mul_assoc sub_eq_add_neg

src/algebra/ring/basic.lean

@@ -231,6 +231,15 @@ end non_unital_semiring
 section non_assoc_semiring
 variables [non_assoc_semiring α]
 
+lemma add_one_mul (a b : α) : (a + 1) * b = a * b + b :=
+by rw [add_mul, one_mul]
+lemma mul_add_one (a b : α) : a * (b + 1) = a * b + a :=
+by rw [mul_add, mul_one]
+lemma one_add_mul (a b : α) : (1 + a) * b = b + a * b :=
+by rw [add_mul, one_mul]
+lemma mul_one_add (a b : α) : a * (1 + b) = a + a * b :=
+by rw [mul_add, mul_one]
+
 theorem two_mul (n : α) : 2 * n = n + n :=
 eq.trans (right_distrib 1 1 n) (by simp)
 
@@ -855,6 +864,15 @@ protected def function.surjective.non_assoc_ring
 { .. hf.add_comm_group f zero add neg sub nsmul gsmul, .. hf.mul_zero_class f zero mul,
   .. hf.distrib f add mul, .. hf.mul_one_class f one mul }
 
+lemma sub_one_mul (a b : α) : (a - 1) * b = a * b - b :=
+by rw [sub_mul, one_mul]
+lemma mul_sub_one (a b : α) : a * (b - 1) = a * b - a :=
+by rw [mul_sub, mul_one]
+lemma one_sub_mul (a b : α) : (1 - a) * b = b - a * b :=
+by rw [sub_mul, one_mul]
+lemma mul_one_sub (a b : α) : a * (1 - b) = a - a * b :=
+by rw [mul_sub, mul_one]
+
 end non_assoc_ring
 
 /-- A ring is a type with the following structures: additive commutative group (`add_comm_group`),