chore(algebra/group/basic): add ite_one_mul and ite_zero_add (#9227)

We already had the versions with the arguments in the other order.

Follows on from #3217

src/algebra/group/basic.lean

@@ -71,6 +71,11 @@ lemma ite_mul_one {P : Prop} [decidable P] {a b : M} :
   ite P (a * b) 1 = ite P a 1 * ite P b 1 :=
 by { by_cases h : P; simp [h], }
 
+@[to_additive]
+lemma ite_one_mul {P : Prop} [decidable P] {a b : M} :
+  ite P 1 (a * b) = ite P 1 a * ite P 1 b :=
+by { by_cases h : P; simp [h], }
+
 @[to_additive]
 lemma eq_one_iff_eq_one_of_mul_eq_one {a b : M} (h : a * b = 1) : a = 1 ↔ b = 1 :=
 by split; { rintro rfl, simpa using h }