mathlib

4a6709bc - feat(data/{int,nat}/gcd): add `nat.gcd_greatest` (#11611)

feat(data/{int,nat}/gcd): add `nat.gcd_greatest` (#11611) Add lemma characterising `gcd` in `ℕ`, counterpart of `int.gcd_greatest`. Also add shorter proof of `int.gcd_greatest`.