Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-27 21:30 a3240c4f

View on Github →

chore(data/nat/basic): split into two files, one not depending on the order hierarchy (#17174)

Estimated changes

deleted theorem nat.add_eq_max_iff
deleted theorem nat.add_eq_min_iff
deleted theorem nat.add_eq_one_iff
deleted theorem nat.add_mod_eq_ite
deleted theorem nat.add_pos_left
deleted theorem nat.add_pos_right
deleted theorem nat.add_succ_lt_add
deleted theorem nat.bit0_le_bit1_iff
deleted theorem nat.bit0_le_bit
deleted theorem nat.bit0_lt_bit1_iff
deleted theorem nat.bit1_le_bit0_iff
deleted theorem nat.bit1_lt_bit0_iff
deleted theorem nat.bit_le
deleted theorem nat.bit_le_bit1
deleted theorem nat.bit_le_bit1_iff
deleted theorem nat.bit_le_bit_iff
deleted theorem nat.bit_lt_bit0
deleted theorem nat.bit_lt_bit
deleted theorem nat.bit_lt_bit_iff
deleted theorem nat.diag_induction
deleted theorem nat.div_div_div_eq_div
deleted theorem nat.div_dvd_of_dvd
deleted theorem nat.div_eq_self
deleted theorem nat.div_eq_sub_mod_div
deleted theorem nat.div_mul_div_comm
deleted theorem nat.div_mul_div_le_div
deleted theorem nat.dvd_div_iff
deleted theorem nat.dvd_div_of_mul_dvd
deleted theorem nat.dvd_iff_div_mul_eq
deleted theorem nat.dvd_iff_dvd_dvd
deleted theorem nat.dvd_iff_le_div_mul
deleted theorem nat.dvd_left_iff_eq
deleted theorem nat.dvd_left_injective
deleted theorem nat.dvd_right_iff_eq
deleted theorem nat.dvd_sub'
deleted theorem nat.dvd_sub_mod
deleted theorem nat.eq_zero_of_double_le
deleted theorem nat.eq_zero_of_dvd_of_lt
deleted theorem nat.eq_zero_of_le_div
deleted theorem nat.eq_zero_of_le_half
deleted theorem nat.eq_zero_of_mul_le
deleted theorem nat.find_add
deleted theorem nat.find_greatest_eq_iff
deleted theorem nat.find_greatest_le
deleted theorem nat.find_greatest_mono
deleted theorem nat.find_greatest_spec
deleted theorem nat.find_pos
deleted theorem nat.le_add_one_iff
deleted theorem nat.le_add_pred_of_pos
deleted theorem nat.le_and_le_add_one_iff
deleted theorem nat.le_find_greatest
deleted theorem nat.le_mul_of_pos_left
deleted theorem nat.le_mul_of_pos_right
deleted theorem nat.le_mul_self
deleted theorem nat.lt_of_lt_pred
deleted theorem nat.lt_one_iff
deleted theorem nat.lt_pred_iff
deleted theorem nat.max_eq_zero_iff
deleted theorem nat.min_eq_zero_iff
deleted theorem nat.mod_div_self
deleted theorem nat.mod_mul_left_div_self
deleted theorem nat.mul_eq_one_iff
deleted theorem nat.mul_self_inj
deleted theorem nat.mul_self_le_mul_self
deleted theorem nat.mul_self_lt_mul_self
deleted theorem nat.not_dvd_of_pos_of_lt
deleted theorem nat.one_le_bit0_iff
deleted theorem nat.one_le_iff_ne_zero
deleted theorem nat.one_le_of_lt
deleted theorem nat.one_lt_bit0_iff
deleted theorem nat.one_mod
deleted theorem nat.pred_le_iff
deleted theorem nat.set_eq_univ
deleted theorem nat.set_induction
deleted theorem nat.set_induction_bounded
deleted theorem nat.sub_succ'
deleted theorem nat.succ_div
deleted theorem nat.succ_div_of_dvd
deleted theorem nat.succ_div_of_not_dvd
deleted theorem nat.succ_mul_pos
deleted theorem nat.two_le_iff
deleted theorem nat.two_mul_odd_div_two
deleted theorem nat.zero_max
added theorem nat.add_eq_max_iff
added theorem nat.add_eq_min_iff
added theorem nat.add_eq_one_iff
added theorem nat.add_mod_eq_ite
added theorem nat.add_pos_left
added theorem nat.add_pos_right
added theorem nat.add_succ_lt_add
added theorem nat.bit0_le_bit1_iff
added theorem nat.bit0_le_bit
added theorem nat.bit0_lt_bit1_iff
added theorem nat.bit1_le_bit0_iff
added theorem nat.bit1_lt_bit0_iff
added theorem nat.bit_le
added theorem nat.bit_le_bit1
added theorem nat.bit_le_bit1_iff
added theorem nat.bit_le_bit_iff
added theorem nat.bit_lt_bit0
added theorem nat.bit_lt_bit
added theorem nat.bit_lt_bit_iff
added theorem nat.diag_induction
added theorem nat.div_div_div_eq_div
added theorem nat.div_dvd_of_dvd
added theorem nat.div_eq_self
added theorem nat.div_eq_sub_mod_div
added theorem nat.div_mul_div_comm
added theorem nat.div_mul_div_le_div
added theorem nat.dvd_div_iff
added theorem nat.dvd_div_of_mul_dvd
added theorem nat.dvd_iff_div_mul_eq
added theorem nat.dvd_iff_dvd_dvd
added theorem nat.dvd_iff_le_div_mul
added theorem nat.dvd_left_iff_eq
added theorem nat.dvd_left_injective
added theorem nat.dvd_right_iff_eq
added theorem nat.dvd_sub'
added theorem nat.dvd_sub_mod
added theorem nat.eq_zero_of_le_div
added theorem nat.eq_zero_of_le_half
added theorem nat.eq_zero_of_mul_le
added theorem nat.find_add
added theorem nat.find_greatest_le
added theorem nat.find_greatest_mono
added theorem nat.find_greatest_spec
added theorem nat.find_pos
added theorem nat.le_add_one_iff
added theorem nat.le_add_pred_of_pos
added theorem nat.le_find_greatest
added theorem nat.le_mul_of_pos_left
added theorem nat.le_mul_self
added theorem nat.lt_of_lt_pred
added theorem nat.lt_one_iff
added theorem nat.lt_pred_iff
added theorem nat.max_eq_zero_iff
added theorem nat.min_eq_zero_iff
added theorem nat.mod_div_self
added theorem nat.mul_eq_one_iff
added theorem nat.mul_self_inj
added theorem nat.one_le_bit0_iff
added theorem nat.one_le_iff_ne_zero
added theorem nat.one_le_of_lt
added theorem nat.one_lt_bit0_iff
added theorem nat.one_mod
added theorem nat.pred_le_iff
added theorem nat.set_eq_univ
added theorem nat.set_induction
added theorem nat.sub_succ'
added theorem nat.succ_div
added theorem nat.succ_div_of_dvd
added theorem nat.succ_mul_pos
added theorem nat.two_le_iff
added theorem nat.zero_max