## 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: May 13 2021 at 22:15 UTC