Zulip Chat Archive

Stream: new members

Topic: 0 = A * B -> 0 = B (a b :ℕ)


view this post on Zulip Rick Love (Aug 17 2020 at 03:12):

This seems like it should be so easy, but I'm not sure how to do this with the natural numbers.

theorem equation_zero_cancel_mul (A B :nat):
    0 = A * B -> 0 = B :=
begin
    intro h,
    sorry,
end

view this post on Zulip Rick Love (Aug 17 2020 at 03:13):

Well it's not true, guess it should be A=0 or B=0

view this post on Zulip Rick Love (Aug 17 2020 at 03:14):

Actually, the assumption is A > 0

view this post on Zulip Rick Love (Aug 17 2020 at 03:14):

theorem equation_zero_cancel_mul (A B :nat) (ha: A > 0):
    0 = A * B -> 0 = B :=
begin
    intro h,
    sorry,
end

view this post on Zulip Adam Topaz (Aug 17 2020 at 03:16):

docs#nat.eq_zero_of_mul_eq_zero should be useful

view this post on Zulip Adam Topaz (Aug 17 2020 at 03:18):

Once you get used to the names of the lemmas/theorems in mathlib, you can search the library here https://leanprover-community.github.io/mathlib_docs

view this post on Zulip Adam Topaz (Aug 17 2020 at 03:23):

There's also https://leanprover-community.github.io/mathlib_docs/tactics.html#library_search

view this post on Zulip Adam Topaz (Aug 17 2020 at 03:24):

And https://leanprover-community.github.io/mathlib_docs/commands.html##find

view this post on Zulip Rick Love (Aug 17 2020 at 03:30):

Ok, figured out how to use that with cases:

theorem equation_zero_cancel_mul (A B :) (ha: A > 0):
    0 = A * B -> 0 = B :=
begin
    intros h,
    cases eq_zero_of_mul_eq_zero h.symm,
    linarith,
    exact h_1.symm,
end

view this post on Zulip Adam Topaz (Aug 17 2020 at 03:38):

You may want to structure your statements so that they are better aligned with the usual conventions of mathlib. E.g. I would change 0=... to ...=0

view this post on Zulip Floris van Doorn (Aug 17 2020 at 04:54):

To expand on that, we try to make the right-hand side of all equalities and iffs to be "simpler" than the left-hand side.
This means most of the time you want to rewrite/simplify, you apply equalities/iffs from left-to-right.


Last updated: May 08 2021 at 04:14 UTC