## 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'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