Result exists?

Stream: maths

[rory]

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]

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]

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]

Hopefully there is a lemma (k ∣ a) ∧ (k ∣ b) ↔ k ∣int.gcd a b. That already gives you one direction.

[Reid Barton]

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]

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

[Floris van Doorn]

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]

oh I tried looking for it in euclidean_domain

[Floris van Doorn]

The single direction exists multiple times, in algebra.euclidean_domain and data.nat.gcd and data.pnat.basic

[rory]

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]

there is almost certainly an analogous theorem for int.gcd

[Mario Carneiro]

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]

or you can use int.coe_gcd to convert gcd to int.gcd