Zulip Chat Archive

Stream: Is there code for X?

Topic: Bezout


view this post on Zulip Alex Kontorovich (Jan 29 2021 at 21:46):

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

view this post on Zulip Aaron Anderson (Jan 29 2021 at 21:59):

Take a look at nat.is_coprime_iff_coprime

view this post on Zulip Aaron Anderson (Jan 29 2021 at 21:59):

docs#nat.is_coprime_iff_coprime

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Alex Kontorovich (Jan 29 2021 at 22:06):

Great thanks! And if aa and bb are integers?...

view this post on Zulip Aaron Anderson (Jan 29 2021 at 22:06):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Aaron Anderson (Jan 29 2021 at 22:19):

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

view this post on Zulip 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]

view this post on Zulip Alex Kontorovich (Jan 30 2021 at 00:56):

Thank you!


Last updated: May 17 2021 at 15:13 UTC