## Stream: Is there code for X?

### Topic: Bezout

#### Alex Kontorovich (Jan 29 2021 at 21:46):

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

#### Aaron Anderson (Jan 29 2021 at 21:59):

Take a look at nat.is_coprime_iff_coprime

#### Aaron Anderson (Jan 29 2021 at 21:59):

docs#nat.is_coprime_iff_coprime

#### Aaron Anderson (Jan 29 2021 at 22:01):

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 (Jan 29 2021 at 22:03):

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

#### Alex Kontorovich (Jan 29 2021 at 22:06):

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

#### Aaron Anderson (Jan 29 2021 at 22:06):

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

#### Aaron Anderson (Jan 29 2021 at 22:06):

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 (Jan 29 2021 at 22:11):

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 (Jan 29 2021 at 22:19):

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

#### Ruben Van de Velde (Jan 29 2021 at 23:12):

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 (Jan 30 2021 at 00:56):

Thank you!

Last updated: May 17 2021 at 15:13 UTC