Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-04-10 15:18
12d0c10f
View on Github →
feat: port Data.Num.Lemmas (
#2784
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Data/Num/Lemmas.lean
added
def
Int.ofSnum
added
theorem
Num.add_ofNat'
added
theorem
Num.add_of_nat
added
theorem
Num.add_one
added
theorem
Num.add_succ
added
theorem
Num.add_toZNum
added
theorem
Num.add_to_nat
added
theorem
Num.add_zero
added
theorem
Num.bit0_of_bit0
added
theorem
Num.bit1_of_bit1
added
theorem
Num.bit1_succ
added
theorem
Num.bit_to_nat
added
theorem
Num.bitwise'_to_nat
added
theorem
Num.cast_add
added
theorem
Num.cast_bit0
added
theorem
Num.cast_bit1
added
theorem
Num.cast_inj
added
theorem
Num.cast_le
added
theorem
Num.cast_lt
added
theorem
Num.cast_mul
added
theorem
Num.cast_ofZNum
added
theorem
Num.cast_one
added
theorem
Num.cast_pos
added
theorem
Num.cast_sub'
added
theorem
Num.cast_succ'
added
theorem
Num.cast_succ
added
theorem
Num.cast_toZNum
added
theorem
Num.cast_toZNumNeg
added
theorem
Num.cast_to_int
added
theorem
Num.cast_to_nat
added
theorem
Num.cast_zero'
added
theorem
Num.cast_zero
added
theorem
Num.cmp_eq
added
theorem
Num.cmp_swap
added
theorem
Num.cmp_to_nat
added
theorem
Num.div_to_nat
added
theorem
Num.dvd_iff_mod_eq_zero
added
theorem
Num.dvd_to_nat
added
theorem
Num.gcd_to_nat
added
theorem
Num.gcd_to_nat_aux
added
theorem
Num.land'_to_nat
added
theorem
Num.ldiff'_to_nat
added
theorem
Num.le_iff_cmp
added
theorem
Num.le_to_nat
added
theorem
Num.lor'_to_nat
added
theorem
Num.lt_iff_cmp
added
theorem
Num.lt_to_nat
added
theorem
Num.lxor'_to_nat
added
theorem
Num.mem_ofZNum'
added
theorem
Num.mod_to_nat
added
theorem
Num.mul_to_nat
added
theorem
Num.natSize_to_nat
added
theorem
Num.ofInt'_toZNum
added
theorem
Num.ofNat'_bit
added
theorem
Num.ofNat'_eq
added
theorem
Num.ofNat'_one
added
theorem
Num.ofNat'_succ
added
theorem
Num.ofNat'_zero
added
theorem
Num.ofZNum'_toNat
added
theorem
Num.ofZNum_toNat
added
theorem
Num.of_nat_cast
added
theorem
Num.of_nat_inj
added
theorem
Num.of_to_nat'
added
theorem
Num.of_to_nat
added
theorem
Num.ppred_to_nat
added
theorem
Num.pred_succ
added
theorem
Num.pred_to_nat
added
theorem
Num.shiftl_to_nat
added
theorem
Num.shiftr_to_nat
added
theorem
Num.size_eq_natSize
added
theorem
Num.size_to_nat
added
theorem
Num.sub_to_nat
added
theorem
Num.succ'_to_nat
added
theorem
Num.succ_ofInt'
added
theorem
Num.succ_to_nat
added
theorem
Num.testBit_to_nat
added
theorem
Num.toZNumNeg_succ
added
theorem
Num.toZNum_inj
added
theorem
Num.toZNum_succ
added
theorem
Num.to_nat_inj
added
theorem
Num.to_nat_to_int
added
theorem
Num.to_of_nat
added
theorem
Num.zero_add
added
theorem
Num.zneg_toZNum
added
theorem
Num.zneg_toZNumNeg
added
theorem
PosNum.add_one
added
theorem
PosNum.add_succ
added
theorem
PosNum.add_to_nat
added
theorem
PosNum.bit0_of_bit0
added
theorem
PosNum.bit1_of_bit1
added
theorem
PosNum.bit_to_nat
added
theorem
PosNum.cast_add
added
theorem
PosNum.cast_bit0
added
theorem
PosNum.cast_bit1
added
theorem
PosNum.cast_inj
added
theorem
PosNum.cast_le
added
theorem
PosNum.cast_lt
added
theorem
PosNum.cast_mul
added
theorem
PosNum.cast_one'
added
theorem
PosNum.cast_one
added
theorem
PosNum.cast_pos
added
theorem
PosNum.cast_sub'
added
theorem
PosNum.cast_succ
added
theorem
PosNum.cast_to_int
added
theorem
PosNum.cast_to_nat
added
theorem
PosNum.cast_to_num
added
theorem
PosNum.cast_to_znum
added
theorem
PosNum.cmp_eq
added
theorem
PosNum.cmp_swap
added
theorem
PosNum.cmp_to_nat
added
theorem
PosNum.cmp_to_nat_lemma
added
theorem
PosNum.div'_to_nat
added
theorem
PosNum.divMod_to_nat
added
theorem
PosNum.divMod_to_nat_aux
added
theorem
PosNum.dvd_to_nat
added
theorem
PosNum.le_iff_cmp
added
theorem
PosNum.le_to_nat
added
theorem
PosNum.lt_iff_cmp
added
theorem
PosNum.lt_to_nat
added
theorem
PosNum.mod'_to_nat
added
theorem
PosNum.mul_to_nat
added
theorem
PosNum.natSize_pos
added
theorem
PosNum.natSize_to_nat
added
theorem
PosNum.of_to_nat'
added
theorem
PosNum.of_to_nat
added
theorem
PosNum.one_add
added
theorem
PosNum.one_le_cast
added
theorem
PosNum.one_sub'
added
theorem
PosNum.pred'_succ'
added
theorem
PosNum.pred'_to_nat
added
theorem
PosNum.pred_to_nat
added
theorem
PosNum.size_eq_natSize
added
theorem
PosNum.size_to_nat
added
theorem
PosNum.sub'_one
added
theorem
PosNum.succ'_pred'
added
theorem
PosNum.succ_to_nat
added
theorem
PosNum.to_int_eq_succ_pred
added
theorem
PosNum.to_nat_eq_succ_pred
added
theorem
PosNum.to_nat_inj
added
theorem
PosNum.to_nat_pos
added
theorem
PosNum.to_nat_to_int
added
theorem
ZNum.abs_toZNum
added
theorem
ZNum.abs_to_nat
added
theorem
ZNum.add_one
added
theorem
ZNum.add_zero
added
theorem
ZNum.bit0_of_bit0
added
theorem
ZNum.bit1_of_bit1
added
theorem
ZNum.cast_add
added
theorem
ZNum.cast_bit0
added
theorem
ZNum.cast_bit1
added
theorem
ZNum.cast_bitm1
added
theorem
ZNum.cast_inj
added
theorem
ZNum.cast_le
added
theorem
ZNum.cast_lt
added
theorem
ZNum.cast_mul
added
theorem
ZNum.cast_neg
added
theorem
ZNum.cast_one
added
theorem
ZNum.cast_pos
added
theorem
ZNum.cast_sub
added
theorem
ZNum.cast_succ
added
theorem
ZNum.cast_to_int
added
theorem
ZNum.cast_zero'
added
theorem
ZNum.cast_zero
added
theorem
ZNum.cast_zneg
added
theorem
ZNum.cmp_to_int
added
theorem
ZNum.div_to_int
added
theorem
ZNum.dvd_iff_mod_eq_zero
added
theorem
ZNum.dvd_to_int
added
theorem
ZNum.gcd_to_nat
added
theorem
ZNum.le_to_int
added
theorem
ZNum.lt_to_int
added
theorem
ZNum.mod_to_int
added
theorem
ZNum.mul_to_int
added
theorem
ZNum.neg_of_int
added
theorem
ZNum.neg_zero
added
theorem
ZNum.ofInt'_eq
added
theorem
ZNum.ofInt'_neg
added
theorem
ZNum.of_int_cast
added
theorem
ZNum.of_nat_cast
added
theorem
ZNum.of_nat_toZNum
added
theorem
ZNum.of_nat_toZNumNeg
added
theorem
ZNum.of_to_int'
added
theorem
ZNum.of_to_int
added
theorem
ZNum.to_int_inj
added
theorem
ZNum.to_of_int
added
theorem
ZNum.zero_add
added
theorem
ZNum.zneg_bit1
added
theorem
ZNum.zneg_bitm1
added
theorem
ZNum.zneg_neg
added
theorem
ZNum.zneg_pos
added
theorem
ZNum.zneg_pred
added
theorem
ZNum.zneg_succ
added
theorem
ZNum.zneg_zneg