feat(algebra/ring): ite_mul_one and ite_mul_zero_... (#3217)

Three simple lemmas about if statements involving multiplication, useful while rewriting.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/group/basic.lean

@@ -11,6 +11,16 @@ import tactic.protected
 
 universe u
 
+section monoid
+variables {M : Type u} [monoid M]
+
+@[to_additive]
+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], }
+
+end monoid
+
 section comm_semigroup
 variables {G : Type u} [comm_semigroup G]
 

src/algebra/ring.lean

@@ -158,6 +158,14 @@ by simp
   (if P then 1 else 0) * a = if P then a else 0 :=
 by simp
 
+lemma ite_mul_zero_left {α : Type*} [mul_zero_class α] (P : Prop) [decidable P] (a b : α) :
+  ite P (a * b) 0 = ite P a 0 * b :=
+by { by_cases h : P; simp [h], }
+
+lemma ite_mul_zero_right {α : Type*} [mul_zero_class α] (P : Prop) [decidable P] (a b : α) :
+  ite P (a * b) 0 = a * ite P b 0 :=
+by { by_cases h : P; simp [h], }
+
 variable (α)
 
 /-- Either zero and one are nonequal in a semiring, or the semiring is the zero ring. -/