mathlib

41dd6d8a - feat(data/nat/modeq): add modeq and dvd lemmas from Apostol Chapter 5 (#11787)

feat(data/nat/modeq): add modeq and dvd lemmas from Apostol Chapter 5 (#11787) Various lemmas about `modeq` from Chapter 5 of Apostol (1976) Introduction to Analytic Number Theory: * `mul_left_iff` and `mul_right_iff`: Apostol, Theorem 5.3 * `dvd_iff_of_modeq_of_dvd`: Apostol, Theorem 5.5 * `gcd_eq_of_modeq`: Apostol, Theorem 5.6 * `eq_of_modeq_of_abs_lt`: Apostol, Theorem 5.7 * `modeq_cancel_left_div_gcd`: Apostol, Theorem 5.4; plus other cancellation lemmas following from this.