Bezout

Stream: Is there code for X?

[Alex Kontorovich]

Is there code to show that $\exists x,y : ax+by=1$ implies $\gcd (a, b) = 1$? Thank you!

[Aaron Anderson]

Take a look at nat.is_coprime_iff_coprime

[Aaron Anderson]

docs#nat.is_coprime_iff_coprime

[Aaron Anderson]

If a and b are natural numbers, but x and y are quantified over the integers, then the left side of that equivalence is your hypothesis, and the right side of that equivalence is defined as nat.gcd a b = 1.

[Aaron Anderson]

If you need a different context, then I think the answer's no, but we could hack it together.

[Alex Kontorovich]

Great thanks! And if $a$ and $b$ are integers?...

[Aaron Anderson]

I think we don't have a particular lemma for that.

[Aaron Anderson]

In that case, the fastest route probably goes through docs#gcd_eq_normalize to reduce it to showing gcd a b | 1, and that should follow from dvd_add and your LHS equation.

[Aaron Anderson]

I think probably the best way to add this into mathlib would be as a converse to euclidean_domain.gcd_eq_gcd_ab, unless using dvd_add is direct enough.

[Aaron Anderson]

Let me know if you think there's a lemma here we should add.

[Ruben Van de Velde]

@Alex Kontorovich how about this?

import data.int.basic
import data.int.parity
import data.nat.gcd
import ring_theory.int.basic

lemma int.gcd_eq_one_iff_coprime' {a b : ℤ} : gcd a b = 1 ↔ is_coprime a b :=
by rw [←int.coe_gcd, ←int.coe_nat_one, int.coe_nat_inj', int.gcd_eq_one_iff_coprime]

[Alex Kontorovich]

Thank you!