mul3_eq_zero

Stream: new members

[Kevin Lacker]

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]

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]

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