Zulip Chat Archive

Stream: new members

Topic: Trouble with nat and int


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

view this post on Zulip Reid Barton (Aug 25 2020 at 17:16):

docs#int.prime.dvd_mul'

view this post on Zulip Marc Masdeu (Aug 25 2020 at 17:17):

Oops sorry! Had overlooked that one...


Last updated: May 14 2021 at 22:15 UTC