# Zulip Chat Archive

## Stream: maths

### Topic: Result exists?

#### rory (Nov 03 2019 at 17:46):

Is there any results in mathlib similar to this, `int.gcd a b = int.gcd c d ↔ ∀ k, (k ∣ a) ∧ (k ∣ b) ↔ (k ∣ c) ∧ (k ∣ d)`

, exist?

#### Kevin Buzzard (Nov 03 2019 at 18:07):

I guess the roadmap to proving this would be to show that away from the edge cases, the gcd is the largest non-negative int dividing both (which might be in mathlib, it sounds like a natural statement) and then use the fact that if two finite sets are equal then so is their largest element.

#### Kevin Buzzard (Nov 03 2019 at 18:08):

My gut feeling is that mathlib is a library of standard results (like the two I mentioned) but then probably it's the user's job to put them together to make statements such as this.

#### Reid Barton (Nov 03 2019 at 22:08):

Hopefully there is a lemma `(k ∣ a) ∧ (k ∣ b) ↔ k ∣int.gcd a b`

. That already gives you one direction.

#### Reid Barton (Nov 03 2019 at 22:09):

For the other direction you need to show that two nonnegative integers which divide each other are equal, which should also be a lemma

#### Kevin Buzzard (Nov 03 2019 at 22:51):

Aah yes this is a much neater way to do it.

#### Floris van Doorn (Nov 04 2019 at 18:53):

The result Reid mentions is

theorem dvd_gcd_iff (a b c : α) : a ∣ gcd b c ↔ (a ∣ b ∧ a ∣ c)

in `algebra.gcd_domain`

#### Kenny Lau (Nov 04 2019 at 18:54):

oh I tried looking for it in `euclidean_domain`

#### Floris van Doorn (Nov 04 2019 at 18:55):

The single direction exists multiple times, in `algebra.euclidean_domain`

and `data.nat.gcd`

and `data.pnat.basic`

#### rory (Nov 06 2019 at 12:15):

The result Reid mentions is

theorem dvd_gcd_iff (a b c : α) : a ∣ gcd b c ↔ (a ∣ b ∧ a ∣ c)in

`algebra.gcd_domain`

How do I eventually convert from `gcd a b`

to `int.gcd`

?

The final result could be proved using `int.antisymm`

, but that requires `int.gcd`

not `gcd`

#### Mario Carneiro (Nov 06 2019 at 12:16):

there is almost certainly an analogous theorem for `int.gcd`

#### Mario Carneiro (Nov 06 2019 at 12:19):

Hm, this particular theorem appears to be missing, but you can reconstruct it from `int.dvd_gcd`

, `int.gcd_dvd_left`

, `int.gcd_dvd_right`

#### Mario Carneiro (Nov 06 2019 at 12:20):

or you can use `int.coe_gcd`

to convert `gcd`

to `int.gcd`

Last updated: May 11 2021 at 16:22 UTC