mathlib

07b578e5 - feat(data/int/basic): add lemma `gcd_greatest` (#10613)

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>