Mathlib v3 is deprecated. Go to Mathlib v4

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 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.

Estimated changes