## Stream: new members

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

#### 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


#### Rick Love (Aug 17 2020 at 03:13):

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

#### Rick Love (Aug 17 2020 at 03:14):

Actually, the assumption is A > 0

#### 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


#### Adam Topaz (Aug 17 2020 at 03:16):

docs#nat.eq_zero_of_mul_eq_zero should be useful

#### 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

#### 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


#### 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

#### 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