Mathlib Changelog
v3
Changelog
About
Github
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
Modified
src/algebra/group_power/basic.lean
Modified
src/algebra/group_power/ring.lean
Modified
src/algebra/order/pi.lean
Modified
src/data/list/basic.lean
Modified
src/data/list/func.lean
Modified
src/data/nat/basic.lean
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_iff_pos_or_pos
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_iff_eq_of_dvd_dvd
deleted
theorem
nat.div_eq_self
deleted
theorem
nat.div_eq_sub_mod_div
deleted
theorem
nat.div_lt_div_of_lt_of_dvd
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_one_of_mul_eq_one_left
deleted
theorem
nat.eq_one_of_mul_eq_one_right
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_eq_zero_iff
deleted
theorem
nat.find_greatest_is_greatest
deleted
theorem
nat.find_greatest_le
deleted
theorem
nat.find_greatest_mono
deleted
theorem
nat.find_greatest_mono_left
deleted
theorem
nat.find_greatest_mono_right
deleted
theorem
nat.find_greatest_of_ne_zero
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.le_or_le_of_add_eq_add_pred
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.mod_mul_right_div_self
deleted
theorem
nat.mul_div_mul_comm_of_dvd_dvd
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_le_mul_self_iff
deleted
theorem
nat.mul_self_lt_mul_self
deleted
theorem
nat.mul_self_lt_mul_self_iff
deleted
theorem
nat.not_dvd_iff_between_consec_multiples
deleted
theorem
nat.not_dvd_of_between_consec_multiples
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_lt_iff_ne_zero_and_ne_one
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_mod_eq_zero_of_mod_eq
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
Modified
src/data/nat/cast.lean
Modified
src/data/nat/dist.lean
Created
src/data/nat/order.lean
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_iff_pos_or_pos
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_iff_eq_of_dvd_dvd
added
theorem
nat.div_eq_self
added
theorem
nat.div_eq_sub_mod_div
added
theorem
nat.div_lt_div_of_lt_of_dvd
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_one_of_mul_eq_one_left
added
theorem
nat.eq_one_of_mul_eq_one_right
added
theorem
nat.eq_zero_of_double_le
added
theorem
nat.eq_zero_of_dvd_of_lt
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_eq_iff
added
theorem
nat.find_greatest_eq_zero_iff
added
theorem
nat.find_greatest_is_greatest
added
theorem
nat.find_greatest_le
added
theorem
nat.find_greatest_mono
added
theorem
nat.find_greatest_mono_left
added
theorem
nat.find_greatest_mono_right
added
theorem
nat.find_greatest_of_ne_zero
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_and_le_add_one_iff
added
theorem
nat.le_find_greatest
added
theorem
nat.le_mul_of_pos_left
added
theorem
nat.le_mul_of_pos_right
added
theorem
nat.le_mul_self
added
theorem
nat.le_or_le_of_add_eq_add_pred
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.mod_mul_left_div_self
added
theorem
nat.mod_mul_right_div_self
added
theorem
nat.mul_div_mul_comm_of_dvd_dvd
added
theorem
nat.mul_eq_one_iff
added
theorem
nat.mul_self_inj
added
theorem
nat.mul_self_le_mul_self
added
theorem
nat.mul_self_le_mul_self_iff
added
theorem
nat.mul_self_lt_mul_self
added
theorem
nat.mul_self_lt_mul_self_iff
added
theorem
nat.not_dvd_iff_between_consec_multiples
added
theorem
nat.not_dvd_of_between_consec_multiples
added
theorem
nat.not_dvd_of_pos_of_lt
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_lt_iff_ne_zero_and_ne_one
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.set_induction_bounded
added
theorem
nat.sub_mod_eq_zero_of_mod_eq
added
theorem
nat.sub_succ'
added
theorem
nat.succ_div
added
theorem
nat.succ_div_of_dvd
added
theorem
nat.succ_div_of_not_dvd
added
theorem
nat.succ_mul_pos
added
theorem
nat.two_le_iff
added
theorem
nat.two_mul_odd_div_two
added
theorem
nat.zero_max
Modified
src/data/nat/psub.lean
Modified
src/data/nat/upto.lean
Modified
src/data/nat/with_bot.lean
Modified
src/data/pnat/basic.lean
Modified
src/order/complete_lattice.lean
Modified
test/library_search/nat.lean
Modified
test/library_search/ordered_ring.lean