# Zulip Chat Archive

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

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

Thank you!

Last updated: May 17 2021 at 15:13 UTC