Zulip Chat Archive

Stream: new members

Topic: euclid_lemma


Brian Jiang (Mar 07 2020 at 23:53):

hey I'm trying to write out the statement for Euclid's lemma (if a and b are relatively prime then there exist integers m and n such that ma + mb = 1); I'm not too familiar with syntax in lean yet, so can someone show me how to write out this statement?

Thanks

Mario Carneiro (Mar 08 2020 at 00:00):

import data.nat.gcd

example {a b : } (h : nat.coprime a b) :  m n : , m * a + n * b = 1 := sorry

Brian Jiang (Mar 08 2020 at 13:49):

thanks! do you know of any good resources for learning basic syntax/tactics in lean?

Donald Sebastian Leung (Mar 08 2020 at 13:51):

Depending on your current competence in Lean, I would recommend either Kevin's natural number game or TPIL

Kevin Buzzard (Mar 08 2020 at 14:31):

Just try and think of a bunch of maths things yourself and try and state them and/or prove them, and ask if you get stuck :-)


Last updated: Dec 20 2023 at 11:08 UTC