Zulip Chat Archive

Stream: maths

Topic: Result exists?


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

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

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

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

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

view this post on Zulip Kevin Buzzard (Nov 03 2019 at 22:51):

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

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

view this post on Zulip Kenny Lau (Nov 04 2019 at 18:54):

oh I tried looking for it in euclidean_domain

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

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

view this post on Zulip Mario Carneiro (Nov 06 2019 at 12:16):

there is almost certainly an analogous theorem for int.gcd

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

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