Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-05 21:51 11613e28

View on Github →

chore(data/int/basic): split file (#17342) This splits data.int.basic into seven files, organised mostly by import requirements.

  • data.int.basic only requires algebra.ring.basic and data.nat.basic
  • data.int.order requires data.int.basic and also algebra.order.ring
  • data.int.bitwise requires data.int.basic and also data.nat.pow
  • data.int.units requires data.int.order and algebra.group_power.order
  • data.int.dvd requires data.int.order, data.nat.cast and data.nat.pow
  • data.int.div requires data.int.dvd and algebra.ring.regular
  • data.int.lemmas contains the remainder, both data.int.order and data.int.bitwise, and also data.nat.cast. To accommodate this I've moved the existing (but unused in mathlib) data.int.order to data.int.conditionally_complete_order. This results in a moderate reduction of import requirements downstream, but I'm hoping to do much better in separate PRs. For now I just want to get this file organised.

Estimated changes

deleted theorem int.abs_div_le_abs
deleted theorem int.abs_eq_nat_abs
deleted theorem int.abs_le_one_iff
deleted theorem int.abs_lt_one_iff
deleted theorem int.abs_sign_of_nonzero
deleted theorem int.add_mod
deleted theorem int.add_mod_mod
deleted theorem int.add_mod_self
deleted theorem int.add_mod_self_left
deleted theorem int.add_mul_mod_self
deleted theorem int.add_mul_mod_self_left
deleted theorem int.bit0_ne_bit1
deleted theorem int.bit0_val
deleted theorem int.bit1_ne_bit0
deleted theorem int.bit1_ne_zero
deleted theorem int.bit1_val
deleted theorem int.bit_coe_nat
deleted theorem int.bit_decomp
deleted theorem int.bit_neg_succ
deleted theorem int.bit_val
deleted theorem int.bit_zero
deleted theorem int.bitwise_and
deleted theorem int.bitwise_bit
deleted theorem int.bitwise_diff
deleted theorem int.bitwise_or
deleted theorem int.bitwise_xor
deleted theorem int.bodd_add
deleted theorem int.bodd_add_div2
deleted theorem int.bodd_bit0
deleted theorem int.bodd_bit1
deleted theorem int.bodd_bit
deleted theorem int.bodd_coe
deleted theorem int.bodd_mul
deleted theorem int.bodd_neg
deleted theorem int.bodd_neg_of_nat
deleted theorem int.bodd_one
deleted theorem int.bodd_sub_nat_nat
deleted theorem int.bodd_two
deleted theorem int.bodd_zero
deleted theorem int.coe_nat_abs
deleted theorem int.coe_nat_dvd
deleted theorem int.coe_nat_dvd_left
deleted theorem int.coe_nat_dvd_right
deleted theorem int.coe_nat_eq_zero
deleted theorem int.coe_nat_ne_zero
deleted theorem int.coe_nat_nonpos_iff
deleted theorem int.coe_nat_pos
deleted theorem int.coe_nat_succ_pos
deleted theorem int.div2_bit
deleted theorem int.div2_val
deleted theorem int.div_dvd_div
deleted theorem int.div_dvd_of_dvd
deleted theorem int.div_eq_zero_of_lt_abs
deleted theorem int.div_le_self
deleted theorem int.div_pos_of_pos_of_dvd
deleted theorem int.dvd_antisymm
deleted theorem int.dvd_div_of_mul_dvd
deleted theorem int.dvd_iff_mod_eq_zero
deleted theorem int.dvd_nat_abs
deleted theorem int.dvd_of_mod_eq_zero
deleted theorem int.dvd_of_pow_dvd
deleted theorem int.dvd_sub_of_mod_eq
deleted theorem int.eq_one_of_dvd_one
deleted theorem int.eq_zero_of_abs_lt_dvd
deleted theorem int.inj_on_nat_abs_Ici
deleted theorem int.inj_on_nat_abs_Iic
deleted theorem int.is_unit_iff_abs_eq
deleted theorem int.is_unit_sq
deleted theorem int.land_bit
deleted theorem int.ldiff_bit
deleted theorem int.le_add_one
deleted theorem int.le_coe_nat_sub
deleted theorem int.le_of_dvd
deleted theorem int.le_sub_one_iff
deleted theorem int.lnot_bit
deleted theorem int.lor_bit
deleted theorem int.lt_add_one_iff
deleted theorem int.lt_of_to_nat_lt
deleted theorem int.lt_succ_self
deleted theorem int.lt_to_nat
deleted theorem int.lxor_bit
deleted theorem int.mod_abs
deleted theorem int.mod_add_cancel_left
deleted theorem int.mod_add_cancel_right
deleted theorem int.mod_add_mod
deleted theorem int.mod_eq_zero_of_dvd
deleted theorem int.mod_lt
deleted theorem int.mod_lt_of_pos
deleted theorem int.mod_mod
deleted theorem int.mod_mod_of_dvd
deleted theorem int.mod_nonneg
deleted theorem int.mod_self
deleted theorem int.mod_sub_cancel_right
deleted theorem int.mul_mod
deleted theorem int.mul_mod_left
deleted theorem int.mul_mod_right
deleted theorem int.nat_abs_abs
deleted theorem int.nat_abs_dvd
deleted theorem int.nat_abs_dvd_iff_dvd
deleted theorem int.nat_abs_eq_iff_sq_eq
deleted theorem int.nat_abs_eq_of_dvd_dvd
deleted theorem int.nat_abs_le_iff_sq_le
deleted theorem int.nat_abs_lt_iff_sq_lt
deleted theorem int.neg_div_of_dvd
deleted theorem int.neg_mod_two
deleted theorem int.neg_one_pow_ne_zero
deleted theorem int.one_le_abs
deleted theorem int.one_shiftl
deleted theorem int.pred_self_lt
deleted theorem int.shiftl_add
deleted theorem int.shiftl_coe_nat
deleted theorem int.shiftl_eq_mul_pow
deleted theorem int.shiftl_neg
deleted theorem int.shiftl_neg_succ
deleted theorem int.shiftl_sub
deleted theorem int.shiftr_add
deleted theorem int.shiftr_coe_nat
deleted theorem int.shiftr_eq_div_pow
deleted theorem int.shiftr_neg
deleted theorem int.shiftr_neg_succ
deleted theorem int.sign_mul_abs
deleted theorem int.sign_pow_bit1
deleted theorem int.sub_div_of_dvd
deleted theorem int.sub_div_of_dvd_sub
deleted theorem int.sub_mod
deleted theorem int.sub_one_lt_iff
deleted theorem int.succ_coe_nat_pos
deleted theorem int.test_bit_bitwise
deleted theorem int.test_bit_land
deleted theorem int.test_bit_ldiff
deleted theorem int.test_bit_lnot
deleted theorem int.test_bit_lor
deleted theorem int.test_bit_lxor
deleted theorem int.test_bit_succ
deleted theorem int.test_bit_zero
deleted theorem int.to_nat_eq_zero
deleted theorem int.to_nat_le
deleted theorem int.to_nat_le_to_nat
deleted theorem int.to_nat_lt_to_nat
deleted theorem int.to_nat_of_nonpos
deleted theorem int.to_nat_sub_of_le
deleted theorem int.units_coe_mul_self
deleted theorem int.units_inv_eq_self
deleted theorem int.units_mul_self
deleted theorem int.units_sq
deleted theorem int.zero_shiftl
deleted theorem int.zero_shiftr
deleted def int.{u}
added theorem int.bit0_ne_bit1
added theorem int.bit0_val
added theorem int.bit1_ne_bit0
added theorem int.bit1_ne_zero
added theorem int.bit1_val
added theorem int.bit_coe_nat
added theorem int.bit_decomp
added theorem int.bit_neg_succ
added theorem int.bit_val
added theorem int.bit_zero
added theorem int.bitwise_and
added theorem int.bitwise_bit
added theorem int.bitwise_diff
added theorem int.bitwise_or
added theorem int.bitwise_xor
added theorem int.bodd_add
added theorem int.bodd_add_div2
added theorem int.bodd_bit0
added theorem int.bodd_bit1
added theorem int.bodd_bit
added theorem int.bodd_coe
added theorem int.bodd_mul
added theorem int.bodd_neg
added theorem int.bodd_neg_of_nat
added theorem int.bodd_one
added theorem int.bodd_sub_nat_nat
added theorem int.bodd_two
added theorem int.bodd_zero
added theorem int.div2_val
added theorem int.land_bit
added theorem int.ldiff_bit
added theorem int.lnot_bit
added theorem int.lor_bit
added theorem int.lxor_bit
added theorem int.one_shiftl
added theorem int.shiftl_add
added theorem int.shiftl_coe_nat
added theorem int.shiftl_eq_mul_pow
added theorem int.shiftl_neg
added theorem int.shiftl_neg_succ
added theorem int.shiftl_sub
added theorem int.shiftr_add
added theorem int.shiftr_coe_nat
added theorem int.shiftr_eq_div_pow
added theorem int.shiftr_neg
added theorem int.shiftr_neg_succ
added theorem int.test_bit_bitwise
added theorem int.test_bit_land
added theorem int.test_bit_ldiff
added theorem int.test_bit_lnot
added theorem int.test_bit_lor
added theorem int.test_bit_lxor
added theorem int.test_bit_succ
added theorem int.test_bit_zero
added theorem int.zero_shiftl
added theorem int.zero_shiftr
added def int.{u}
added theorem int.coe_nat_pos
added theorem int.coe_nat_succ_pos
added theorem int.cInf_empty
added theorem int.cInf_mem
added theorem int.cSup_empty
added theorem int.cSup_mem
added theorem int.coe_nat_dvd
added theorem int.coe_nat_dvd_left
added theorem int.coe_nat_dvd_right
added theorem int.dvd_antisymm
added theorem int.dvd_of_pow_dvd
added theorem int.eq_one_of_dvd_one
added theorem int.le_of_dvd
added theorem int.sign_pow_bit1
added theorem int.div2_bit
added theorem int.inj_on_nat_abs_Ici
added theorem int.inj_on_nat_abs_Iic
added theorem int.le_coe_nat_sub
added theorem int.succ_coe_nat_pos
added theorem int.to_nat_of_nonpos
added theorem int.abs_div_le_abs
added theorem int.abs_eq_nat_abs
added theorem int.abs_le_one_iff
added theorem int.abs_lt_one_iff
added theorem int.add_mod
added theorem int.add_mod_mod
added theorem int.add_mod_self
added theorem int.add_mod_self_left
added theorem int.add_mul_mod_self
deleted theorem int.cInf_empty
deleted theorem int.cInf_eq_least_of_bdd
deleted theorem int.cInf_mem
deleted theorem int.cInf_of_not_bdd_below
deleted theorem int.cSup_empty
deleted theorem int.cSup_mem
deleted theorem int.cSup_of_not_bdd_above
added theorem int.coe_nat_abs
added theorem int.coe_nat_eq_zero
added theorem int.coe_nat_ne_zero
added theorem int.coe_nat_nonpos_iff
added theorem int.div_dvd_div
added theorem int.div_dvd_of_dvd
added theorem int.div_le_self
added theorem int.dvd_div_of_mul_dvd
added theorem int.dvd_nat_abs
added theorem int.dvd_of_mod_eq_zero
added theorem int.dvd_sub_of_mod_eq
added theorem int.is_unit_iff_abs_eq
added theorem int.le_add_one
added theorem int.le_sub_one_iff
added theorem int.lt_add_one_iff
added theorem int.lt_of_to_nat_lt
added theorem int.lt_succ_self
added theorem int.lt_to_nat
added theorem int.mod_abs
added theorem int.mod_add_mod
added theorem int.mod_eq_zero_of_dvd
added theorem int.mod_lt
added theorem int.mod_lt_of_pos
added theorem int.mod_mod
added theorem int.mod_mod_of_dvd
added theorem int.mod_nonneg
added theorem int.mod_self
added theorem int.mul_mod
added theorem int.mul_mod_left
added theorem int.mul_mod_right
added theorem int.nat_abs_abs
added theorem int.nat_abs_dvd
added theorem int.neg_div_of_dvd
added theorem int.neg_mod_two
added theorem int.one_le_abs
added theorem int.pred_self_lt
added theorem int.sign_mul_abs
added theorem int.sub_div_of_dvd
added theorem int.sub_div_of_dvd_sub
added theorem int.sub_mod
added theorem int.sub_one_lt_iff
added theorem int.to_nat_eq_zero
added theorem int.to_nat_le
added theorem int.to_nat_le_to_nat
added theorem int.to_nat_lt_to_nat
added theorem int.to_nat_sub_of_le
added theorem int.is_unit_sq
added theorem int.units_coe_mul_self
added theorem int.units_inv_eq_self
added theorem int.units_mul_self
added theorem int.units_sq