Zulip Chat Archive

Stream: new members

Topic: euclid_lemma

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


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

view this post on Zulip Brian Jiang (Mar 08 2020 at 13:49):

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

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

view this post on Zulip 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: May 13 2021 at 22:15 UTC