Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-20 22:33 b2d95c0c

View on Github →

feat(data/nat/modeq): Generalised version of the Chinese remainder theorem (#5683) That allows the moduli to not be coprime, assuming the necessary condition. Old crt is now in terms of this one

Estimated changes

Modified src/algebra/euclidean_domain.lean

added theorem euclidean_domain.gcd_a_zero_left

added theorem euclidean_domain.gcd_b_zero_left

Modified src/data/int/basic.lean

added theorem int.sub_div_of_dvd

added theorem int.sub_div_of_dvd_sub

Modified src/data/int/gcd.lean

added theorem nat.gcd_a_zero_left

added theorem nat.gcd_a_zero_right

added theorem nat.gcd_b_zero_left

added theorem nat.gcd_b_zero_right

Modified src/data/nat/gcd.lean

added theorem nat.gcd_eq_zero_iff

added theorem nat.lcm_ne_zero

Modified src/data/nat/modeq.lean

added def nat.modeq.chinese_remainder'

added theorem nat.modeq.modeq_one