## Stream: new members

### Topic: Trouble with nat and int

#### Marc Masdeu (Aug 25 2020 at 17:12):

Hi,

What is the one-liner that proves the following lemma?

variables {p : ℕ} [fact p.prime]
lemma euclid_int {a b : ℤ} : (p : ℤ) ∣ (a * b)  → (p : ℤ) ∣ a ∨ (p : ℤ) ∣ b :=
begin
sorry
end


Definitely want to use nat.prime.dvd_mul, BTW. I tried push_cast, norm_cast, and all the _cast family that I could think of, with no luck... Thanks!

#### Reid Barton (Aug 25 2020 at 17:16):

docs#int.prime.dvd_mul'

#### Marc Masdeu (Aug 25 2020 at 17:17):

Oops sorry! Had overlooked that one...

Last updated: May 14 2021 at 22:15 UTC