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