## Stream: new members

### Topic: mul3_eq_zero

#### Kevin Lacker (Oct 07 2020 at 21:12):

I found myself needing a three-variable version of mul_eq_zero. Is this the sort of thing that should go in mathlib, or no, or is there some simpler way to do this?

lemma mul3_eq_zero {x y z : ℝ} : x * y * z = 0 ↔ x = 0 ∨ y = 0 ∨ z = 0 :=
begin
split,
{ intro h1,
have h2 : x * y = 0 ∨ z = 0, from mul_eq_zero.mp h1,
cases h2,
{ have h3 : x = 0 ∨ y = 0, from mul_eq_zero.mp h2,
finish },
{ finish } },
{ intro h4,
cases h4,
{ rw h4, ring },
{ cases h4,
{ rw h4, ring },
{ rw h4, ring } } }
end


#### Yakov Pechersky (Oct 07 2020 at 21:14):

lemma mul3_eq_zero {x y z : ℝ} : x * y * z = 0 ↔ x = 0 ∨ y = 0 ∨ z = 0 :=
by simp only [mul_assoc, mul_eq_zero]


#### Kevin Lacker (Oct 07 2020 at 21:16):

all right, well i can inline that instead of the lemma.

Last updated: May 14 2021 at 12:18 UTC