Commit 2022-12-31 21:27 adabcfd7

View on Github →

feat: port Data.Nat.ModEq (#1274)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/ModEq.lean

added theorem Dvd.dvd.modEq_zero_nat

added theorem Dvd.dvd.zero_modEq_nat

added theorem Nat.ModEq.add_le_of_lt

added theorem Nat.ModEq.dvd_iff_of_modEq_of_dvd

added theorem Nat.ModEq.eq_of_modEq_of_abs_lt

added theorem Nat.ModEq.gcd_eq_of_modEq

added theorem Nat.ModEq.le_of_lt_add

added theorem Nat.ModEq.modEq_cancel_left_div_gcd'

added theorem Nat.ModEq.modEq_cancel_left_div_gcd

added theorem Nat.ModEq.modEq_cancel_left_of_coprime

added theorem Nat.ModEq.modEq_cancel_right_div_gcd'

added theorem Nat.ModEq.modEq_cancel_right_div_gcd

added theorem Nat.ModEq.modEq_cancel_right_of_coprime

added theorem Nat.ModEq.of_modEq_mul_left

added theorem Nat.ModEq.of_modEq_mul_right

added def Nat.ModEq

added theorem Nat.add_div

added theorem Nat.add_div_eq_of_add_mod_lt

added theorem Nat.add_div_eq_of_le_mod_add_mod

added theorem Nat.add_div_le_add_div

added theorem Nat.add_modEq_left

added theorem Nat.add_modEq_right

added theorem Nat.add_mod_add_ite

added theorem Nat.add_mod_add_of_le_add_mod

added theorem Nat.add_mod_of_add_mod_lt

added def Nat.chineseRemainder'

added theorem Nat.chineseRemainder'_lt_lcm

added def Nat.chineseRemainder

added theorem Nat.chineseRemainder_lt_mul

added theorem Nat.coprime_of_mul_modEq_one

added theorem Nat.div_mod_eq_mod_mul_div

added theorem Nat.le_mod_add_mod_of_dvd_add_of_not_dvd

added theorem Nat.modEq_and_modEq_iff_modEq_mul

added theorem Nat.modEq_iff_dvd'

added theorem Nat.modEq_iff_dvd

added theorem Nat.modEq_of_dvd

added theorem Nat.modEq_one

added theorem Nat.modEq_sub

added theorem Nat.modEq_zero_iff

added theorem Nat.modEq_zero_iff_dvd

added theorem Nat.mod_modEq

added theorem Nat.mod_mul_left_mod

added theorem Nat.mod_mul_right_mod

added theorem Nat.odd_mod_four_iff

added theorem Nat.odd_mul_odd

added theorem Nat.odd_mul_odd_div_two

added theorem Nat.odd_of_mod_four_eq_one

added theorem Nat.odd_of_mod_four_eq_three