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)
Kenny Lau (Nov 04 2019 at 18:54):
oh I tried looking for it in
Floris van Doorn (Nov 04 2019 at 18:55):
The single direction exists multiple times, in
rory (Nov 06 2019 at 12:15):
The result Reid mentions istheorem dvd_gcd_iff (a b c : α) : a ∣ gcd b c ↔ (a ∣ b ∧ a ∣ c)
How do I eventually convert from
gcd a b to
The final result could be proved using
int.antisymm, but that requires
Mario Carneiro (Nov 06 2019 at 12:16):
there is almost certainly an analogous theorem for
Mario Carneiro (Nov 06 2019 at 12:19):
Hm, this particular theorem appears to be missing, but you can reconstruct it from
Mario Carneiro (Nov 06 2019 at 12:20):
or you can use
int.coe_gcd to convert
Last updated: May 11 2021 at 16:22 UTC