Zulip Chat Archive

Stream: new members

Topic: mul3_eq_zero


view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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