From 5b75f5ac2a1897f514941f95665f83480959026b Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 17 Sep 2021 09:52:16 +0000
Subject: [PATCH] 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 | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/algebra/group/basic.lean b/src/algebra/group/basic.lean
index 46d906ddb2aa7..895dc042af28a 100644
--- a/src/algebra/group/basic.lean
+++ b/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 }