feat(data/int/basic): add lemma gcd_greatest (#10613)

Proving a uniqueness property for `gcd`.  This is (a version of) Theorem 1.3 in Apostol (1976) Introduction to Analytic Number Theory.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/gcd_monoid/basic.lean

@@ -524,6 +524,22 @@ theorem exists_eq_pow_of_mul_eq_pow [gcd_monoid α] [unique (units α)] {a b c :
   (h : a * b = c ^ k) : ∃ (d : α), a = d ^ k :=
 let ⟨d, hd⟩ := exists_associated_pow_of_mul_eq_pow hab h in ⟨d, (associated_iff_eq.mp hd).symm⟩
 
+lemma gcd_greatest {α : Type*} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α]
+  {a b d : α} (hda : d ∣ a) (hdb : d ∣ b)
+  (hd : ∀ e : α, e ∣ a → e ∣ b → e ∣ d) : gcd_monoid.gcd a b = normalize d :=
+begin
+  have h := hd _ (gcd_monoid.gcd_dvd_left a b) (gcd_monoid.gcd_dvd_right a b),
+  exact gcd_eq_normalize h (gcd_monoid.dvd_gcd hda hdb),
+end
+
+lemma gcd_greatest_associated {α : Type*} [cancel_comm_monoid_with_zero α] [gcd_monoid α]
+  {a b d : α} (hda : d ∣ a) (hdb : d ∣ b)
+  (hd : ∀ e : α, e ∣ a → e ∣ b → e ∣ d) : associated d (gcd_monoid.gcd a b) :=
+begin
+  have h := hd _ (gcd_monoid.gcd_dvd_left a b) (gcd_monoid.gcd_dvd_right a b),
+  exact associated_of_dvd_dvd (gcd_monoid.dvd_gcd hda hdb) h,
+end
+
 end gcd
 
 section lcm

src/data/int/gcd.lean

@@ -302,6 +302,11 @@ begin
   exact int.nat_abs_dvd_iff_dvd.mpr h
 end
 
+lemma gcd_greatest {a b d : ℤ} (hd_pos : 0 ≤ d) (hda : d ∣ a) (hdb : d ∣ b)
+  (hd : ∀ e : ℤ, e ∣ a → e ∣ b → e ∣ d) : d = gcd a b :=
+(nat_abs_inj_of_nonneg_of_nonneg hd_pos (coe_zero_le (gcd a b))).mp
+  (nat_abs_eq_of_dvd_dvd (dvd_gcd hda hdb) (hd _ (gcd_dvd_left a b) (gcd_dvd_right a b)))
+
 /-- Euclid's lemma: if `a ∣ b * c` and `gcd a c = 1` then `a ∣ b`.
 Compare with `is_coprime.dvd_of_dvd_mul_left` and
 `unique_factorization_monoid.dvd_of_dvd_mul_left_of_no_prime_factors` -/