euclid_lemma

Stream: new members

[Brian Jiang]

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]

import data.nat.gcd

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

[Brian Jiang]

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

[Donald Sebastian Leung]

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

[Kevin Buzzard]

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 :-)