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

Stream: new members

[Rick Love]

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

[Rick Love]

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

[Rick Love]

Actually, the assumption is A > 0

[Rick Love]

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

[Adam Topaz]

docs#nat.eq_zero_of_mul_eq_zero should be useful

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Rick Love]

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

[Adam Topaz]

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

[Floris van Doorn]

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.