# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: different gcd's?

#### Alex Kontorovich (Feb 12 2021 at 22:16):

Hello, is there code identifying these two gcds? Thanks!

```
import ring_theory.int.basic
lemma come_on (cc dd : ℤ ) : euclidean_domain.gcd cc dd = gcd cc dd :=
begin
sorry,
end
```

#### Alex J. Best (Feb 12 2021 at 22:23):

Unfortunately it's not true!

```
import ring_theory.int.basic
import tactic.slim_check
lemma come_on (cc dd : ℤ ) : euclidean_domain.gcd cc dd = gcd cc dd :=
begin
slim_check
end
```

reports

```
===================
Found problems!
cc := 0
dd := -1
issue: -1 = 1 does not hold
(1 shrinks)
-------------------
```

#### Mario Carneiro (Feb 12 2021 at 22:24):

It is surprising there is no theorem about this though

#### Mario Carneiro (Feb 12 2021 at 22:24):

it's not hard to prove they are equal up to sign, because they both satisfy the universal property of gcd

#### Mario Carneiro (Feb 12 2021 at 22:25):

but I'm not sure the exact rules of the sign of `euclidean_domain.gcd`

are important to pin down

#### Alex Kontorovich (Feb 12 2021 at 22:31):

Ah ok, thanks. Is there a lemma that they agree up to sign?

#### Alex J. Best (Feb 12 2021 at 22:32):

I didn't see any, hopefully it shouldn't be too hard to prove, but it might depend a bit on what version is needed for your application.

#### Mario Carneiro (Feb 12 2021 at 22:39):

```
import algebra.euclidean_domain data.int.gcd
example (a b : ℤ) : int.nat_abs (euclidean_domain.gcd a b) = int.gcd a b :=
begin
apply nat.dvd_antisymm; rw ← int.coe_nat_dvd,
{ rw int.nat_abs_dvd,
exact int.dvd_gcd (euclidean_domain.gcd_dvd_left _ _) (euclidean_domain.gcd_dvd_right _ _) },
{ rw int.dvd_nat_abs,
exact euclidean_domain.dvd_gcd (int.gcd_dvd_left _ _) (int.gcd_dvd_right _ _) }
end
```

#### Mario Carneiro (Feb 12 2021 at 22:50):

After some mathematica explorations, looks like this is the sign:

```
import algebra.euclidean_domain tactic.slim_check
example (a b : ℤ) : to_bool (euclidean_domain.gcd a b < 0 ↔ a = 0 ∧ b < 0 ∨ a < 0 ∧ a ∣ b) :=
by slim_check
```

#### Paul van Wamelen (Feb 12 2021 at 23:01):

We have

`lemma nat_abs_gcd (i j : ℤ) : nat_abs (gcd_monoid.gcd i j) = int.gcd i j := rfl`

in `ring_theory/int/basic.lean`

.

#### Mario Carneiro (Feb 12 2021 at 23:04):

that's evidently a different function, though, since it's true by refl

#### Mario Carneiro (Feb 12 2021 at 23:04):

to wit:

```
lemma coe_gcd (i j : ℤ) : ↑(int.gcd i j) = gcd_monoid.gcd i j := rfl
```

#### Mario Carneiro (Feb 12 2021 at 23:05):

however there might be a theorem relating `euclidean_domain.gcd`

and `gcd_domain.gcd`

when they both apply

#### Alex Kontorovich (Feb 13 2021 at 01:14):

Great thanks! Followup question: I started using `euclidean_domain.gcd`

because there's a function `euclidean_domain.gcd_a`

etc, which I don't see in `int.gcd`

? Or am I just missing something? Thanks!

#### Mario Carneiro (Feb 13 2021 at 01:42):

```
import data.int.gcd
namespace int
def gcd_a : ℤ → ℤ → ℤ
| (of_nat m) n := m.gcd_a n.nat_abs
| -[1+ m] n := -m.succ.gcd_a n.nat_abs
def gcd_b : ℤ → ℤ → ℤ
| m (of_nat n) := m.nat_abs.gcd_b n
| m -[1+ n] := -m.nat_abs.gcd_b n.succ
theorem gcd_eq_gcd_ab (x y : ℤ) : (gcd x y : ℤ) = x * gcd_a x y + y * gcd_b x y :=
begin
cases x; cases y,
{ apply nat.gcd_eq_gcd_ab },
{ change (_ : ℤ) = _ + -y.succ * -_, rw neg_mul_neg,
apply nat.gcd_eq_gcd_ab },
{ change (_ : ℤ) = -x.succ * -_ + _, rw neg_mul_neg,
apply nat.gcd_eq_gcd_ab },
{ change (_ : ℤ) = -x.succ * -_ + -y.succ * -_, rw [neg_mul_neg, neg_mul_neg],
apply nat.gcd_eq_gcd_ab },
end
end int
```

#### Mario Carneiro (Feb 13 2021 at 01:57):

added in #6212

Last updated: May 19 2021 at 03:22 UTC