Commit 2022-02-15 15:52 41dd6d8a
View on Github →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
andmul_right_iff
: Apostol, Theorem 5.3dvd_iff_of_modeq_of_dvd
: Apostol, Theorem 5.5gcd_eq_of_modeq
: Apostol, Theorem 5.6eq_of_modeq_of_abs_lt
: Apostol, Theorem 5.7modeq_cancel_left_div_gcd
: Apostol, Theorem 5.4; plus other cancellation lemmas following from this.