Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2017-10-24 22:31
dd9f766f
View on Github →
feat(data/num,data/nat/cast,...): nat,num,int,rat.cast, list stuff
Estimated changes
Modified
algebra/field.lean
added
theorem
inv_comm_of_comm
Modified
algebra/group.lean
added
theorem
eq_inv_iff_mul_eq_one
modified
theorem
eq_inv_mul_iff_mul_eq
modified
theorem
eq_mul_inv_iff_mul_eq
modified
theorem
eq_sub_iff_add_eq
added
theorem
inv_eq_iff_mul_eq_one
modified
theorem
inv_mul_eq_iff_eq_mul
modified
theorem
mul_inv_eq_iff_eq_mul
Modified
algebra/group_power.lean
added
theorem
nat.pow_eq_pow_nat
Modified
algebra/ordered_ring.lean
added
theorem
mul_nonneg_iff_right_nonneg_of_pos
Modified
analysis/limits.lean
modified
theorem
mul_add_one_le_pow
Modified
analysis/measure_theory/lebesgue_measure.lean
modified
theorem
measure_theory.tendsto_of_nat_at_top_at_top
Modified
analysis/metric_space.lean
Deleted
analysis/of_nat.lean
deleted
theorem
exists_lt_of_nat
deleted
theorem
int_of_nat_eq_of_nat
deleted
def
of_nat
deleted
theorem
of_nat_add
deleted
theorem
of_nat_bit0
deleted
theorem
of_nat_bit1
deleted
theorem
of_nat_le_of_nat
deleted
theorem
of_nat_le_of_nat_iff
deleted
theorem
of_nat_mul
deleted
theorem
of_nat_one
deleted
theorem
of_nat_pos
deleted
theorem
of_nat_sub
deleted
theorem
rat_coe_eq_of_nat
deleted
theorem
rat_of_nat_eq_of_nat
deleted
theorem
real_of_rat_of_nat_eq_of_nat
deleted
theorem
zero_le_of_nat
Modified
analysis/real.lean
added
theorem
coe_rat_eq_of_rat
added
theorem
exists_lt_nat
modified
def
lift_rat_fun
modified
def
lift_rat_op
Modified
data/encodable.lean
modified
def
encodable_of_equiv
Modified
data/equiv.lean
added
theorem
equiv.apply_inverse_apply
added
def
equiv.int_equiv_nat
added
def
equiv.int_equiv_nat_sum_nat
added
def
equiv.psigma_equiv_sigma
added
def
equiv.psum_equiv_sum
added
def
equiv.sigma_congr_left
added
def
equiv.sigma_congr_right
added
def
equiv.sigma_equiv_prod
added
def
equiv.sigma_equiv_prod_of_equiv
Modified
data/finset/basic.lean
Modified
data/int/basic.lean
added
theorem
int.cast_add
added
theorem
int.cast_bit0
added
theorem
int.cast_bit1
added
theorem
int.cast_coe_nat
added
theorem
int.cast_eq_zero
added
theorem
int.cast_id
added
theorem
int.cast_inj
added
theorem
int.cast_le
added
theorem
int.cast_lt
added
theorem
int.cast_lt_zero
added
theorem
int.cast_mul
added
theorem
int.cast_ne_zero
added
theorem
int.cast_neg
added
theorem
int.cast_neg_of_nat
added
theorem
int.cast_neg_succ_of_nat
added
theorem
int.cast_nonneg
added
theorem
int.cast_nonpos
added
theorem
int.cast_of_nat
added
theorem
int.cast_one
added
theorem
int.cast_pos
added
theorem
int.cast_sub
added
theorem
int.cast_sub_nat_nat
added
theorem
int.cast_zero
added
theorem
int.coe_nat_dvd
deleted
theorem
int.coe_nat_dvd_coe_nat_iff
deleted
theorem
int.coe_nat_dvd_coe_nat_of_dvd
deleted
theorem
int.coe_nat_dvd_left
deleted
theorem
int.coe_nat_dvd_right
added
theorem
int.coe_nat_eq_zero
added
theorem
int.coe_nat_inj'
added
theorem
int.coe_nat_le
added
theorem
int.coe_nat_lt
added
theorem
int.coe_nat_ne_zero
added
theorem
int.coe_nat_pos
added
theorem
int.dvd_nat_abs
deleted
theorem
int.dvd_of_coe_nat_dvd_coe_nat
added
theorem
int.mul_cast_comm
added
theorem
int.nat_abs_dvd
added
theorem
int.nat_cast_eq_coe_nat
Modified
data/list/basic.lean
added
theorem
list.diff_cons
added
theorem
list.diff_eq_foldl
added
theorem
list.diff_nil
added
theorem
list.erase_comm
Modified
data/list/perm.lean
added
theorem
list.count_le_of_subperm
added
theorem
list.countp_le_of_subperm
added
theorem
list.exists_perm_append_of_sublist
deleted
theorem
list.exists_sublist_perm_of_subset_nodup
added
theorem
list.length_le_of_subperm
deleted
theorem
list.mem_iff_mem_of_perm
modified
theorem
list.mem_of_perm
added
theorem
list.perm.subperm_left
added
theorem
list.perm.subperm_right
deleted
theorem
list.perm_app_inv_right
added
theorem
list.perm_app_right_iff
added
theorem
list.perm_diff_left
added
theorem
list.perm_diff_right
added
theorem
list.perm_subset
added
theorem
list.subperm.antisymm
added
theorem
list.subperm.exists_of_length_lt
added
theorem
list.subperm.perm_of_length_le
added
theorem
list.subperm.refl
added
theorem
list.subperm.trans
added
def
list.subperm
added
theorem
list.subperm_app_left
added
theorem
list.subperm_app_right
added
theorem
list.subperm_cons
added
theorem
list.subperm_of_perm
added
theorem
list.subperm_of_sublist
added
theorem
list.subperm_of_subset_nodup
added
theorem
list.subset_of_subperm
Modified
data/list/sort.lean
Created
data/nat/cast.lean
added
theorem
nat.cast_add
added
theorem
nat.cast_add_one
added
theorem
nat.cast_bit0
added
theorem
nat.cast_bit1
added
theorem
nat.cast_eq_zero
added
theorem
nat.cast_id
added
theorem
nat.cast_inj
added
theorem
nat.cast_le
added
theorem
nat.cast_lt
added
theorem
nat.cast_mul
added
theorem
nat.cast_ne_zero
added
theorem
nat.cast_nonneg
added
theorem
nat.cast_one
added
theorem
nat.cast_pos
added
theorem
nat.cast_pred
added
theorem
nat.cast_sub
added
theorem
nat.cast_succ
added
theorem
nat.cast_zero
added
theorem
nat.mul_cast_comm
Modified
data/num/basic.lean
deleted
def
int.of_znum
deleted
def
int.znum_coe
deleted
def
nat.of_num
deleted
def
nat.of_pos_num
deleted
def
num.nat_num_coe
modified
def
nzsnum.drec'
modified
def
snum.drec'
added
def
znum.cmp
Modified
data/num/bitwise.lean
Modified
data/num/lemmas.lean
deleted
theorem
num.add_to_nat
added
theorem
num.cast_add
added
theorem
num.cast_cmp'
added
theorem
num.cast_cmp
added
theorem
num.cast_inj
added
theorem
num.cast_le
added
theorem
num.cast_lt
added
theorem
num.cast_mul
added
theorem
num.cast_one
added
theorem
num.cast_succ'
added
theorem
num.cast_succ
added
theorem
num.cast_zero
deleted
theorem
num.cmp_dec
added
theorem
num.cmp_eq
modified
theorem
num.lt_iff_cmp
deleted
theorem
num.mul_to_nat
deleted
theorem
num.one_to_nat
deleted
theorem
num.succ'_to_nat
deleted
theorem
num.succ_to_nat
deleted
theorem
num.zero_to_nat
deleted
theorem
pos_num.add_to_nat
added
theorem
pos_num.cast_add
added
theorem
pos_num.cast_add_comm
added
theorem
pos_num.cast_add_comm_lemma_1
added
theorem
pos_num.cast_add_comm_lemma_2
added
theorem
pos_num.cast_add_one_comm
added
theorem
pos_num.cast_cmp'
added
theorem
pos_num.cast_cmp
added
theorem
pos_num.cast_inj
added
theorem
pos_num.cast_le
added
theorem
pos_num.cast_lt
added
theorem
pos_num.cast_mul
added
theorem
pos_num.cast_one
added
theorem
pos_num.cast_pos
added
theorem
pos_num.cast_succ
deleted
theorem
pos_num.cmp_dec
deleted
theorem
pos_num.cmp_dec_theorem
added
theorem
pos_num.cmp_eq
modified
theorem
pos_num.lt_iff_cmp
deleted
theorem
pos_num.mul_to_nat
added
theorem
pos_num.one_le_cast
deleted
theorem
pos_num.one_to_nat
deleted
theorem
pos_num.succ_to_nat
modified
theorem
pos_num.to_nat_inj
deleted
theorem
pos_num.to_nat_pos
added
theorem
znum.cast_one
added
theorem
znum.cast_zero
Deleted
data/num/norm_num.lean
deleted
theorem
norm_num.bit0_le_one
deleted
theorem
norm_num.bit0_le_zero
deleted
theorem
norm_num.bit1_le_bit0
deleted
theorem
norm_num.bit1_le_one
deleted
theorem
norm_num.bit1_le_zero
deleted
theorem
norm_num.one_le_bit0
deleted
theorem
norm_num.one_le_bit1
deleted
theorem
norm_num.one_le_one
deleted
theorem
norm_num.pow_bit0
deleted
theorem
norm_num.pow_bit0_helper
deleted
theorem
norm_num.pow_bit1
deleted
theorem
norm_num.pow_bit1_helper
deleted
theorem
norm_num.pow_eq_pow_nat
deleted
theorem
norm_num.pow_eq_pow_nat_helper
deleted
theorem
norm_num.pow_one
deleted
theorem
norm_num.pow_zero
deleted
theorem
norm_num.zero_le_bit0
deleted
theorem
norm_num.zero_le_bit1
deleted
theorem
norm_num.zero_le_one
deleted
theorem
norm_num.zero_le_zero
deleted
def
num.add1
deleted
def
num.add_n
deleted
theorem
num.bit0_le_bit0
deleted
theorem
num.denote_add1
deleted
theorem
num.denote_le_denote_of_num_le
deleted
theorem
num.denote_le_denote_of_pos_num_le
deleted
theorem
num.denote_le_denote_of_znum_le
deleted
def
num.num_le
deleted
theorem
num.one_le_denote
deleted
def
num.pos_le
deleted
theorem
num.zero_le_denote
deleted
def
num.znum_le
deleted
inductive
tactic.interactive.denotation
deleted
def
tactic.interactive.znum.to_neg
deleted
def
tactic.interactive.znum.to_pos
Modified
data/option.lean
added
theorem
option.bind_eq_some
added
theorem
option.bind_none
modified
theorem
option.bind_some
modified
def
option.filter
modified
def
option.guard
modified
theorem
option.guard_eq_some
modified
def
option.iget
added
theorem
option.is_some_iff_exists
added
theorem
option.map_eq_some
added
theorem
option.map_none
added
theorem
option.map_some
modified
theorem
option.mem_def
added
theorem
option.none_ne_some
modified
theorem
option.some_inj
Modified
data/rat.lean
deleted
def
linear_order_cases_on
deleted
theorem
linear_order_cases_on_eq
deleted
theorem
linear_order_cases_on_gt
deleted
theorem
linear_order_cases_on_lt
deleted
theorem
mul_nonneg_iff_right_nonneg_of_pos
added
theorem
rat.cast_add
added
theorem
rat.cast_add_of_ne_zero
added
theorem
rat.cast_bit0
added
theorem
rat.cast_bit1
added
theorem
rat.cast_coe_int
added
theorem
rat.cast_coe_nat
added
theorem
rat.cast_eq_zero
added
theorem
rat.cast_id
added
theorem
rat.cast_inj
added
theorem
rat.cast_le
added
theorem
rat.cast_lt
added
theorem
rat.cast_lt_zero
added
theorem
rat.cast_mk
added
theorem
rat.cast_mk_of_ne_zero
added
theorem
rat.cast_mul
added
theorem
rat.cast_mul_of_ne_zero
added
theorem
rat.cast_ne_zero
added
theorem
rat.cast_neg
added
theorem
rat.cast_nonneg
added
theorem
rat.cast_nonpos
added
theorem
rat.cast_of_int
added
theorem
rat.cast_one
added
theorem
rat.cast_pos
added
theorem
rat.cast_sub
added
theorem
rat.cast_sub_of_ne_zero
added
theorem
rat.cast_zero
deleted
theorem
rat.coe_int_add
modified
theorem
rat.coe_int_eq_mk
added
theorem
rat.coe_int_eq_of_int
deleted
theorem
rat.coe_int_inj
deleted
theorem
rat.coe_int_le
deleted
theorem
rat.coe_int_lt
deleted
theorem
rat.coe_int_mul
deleted
theorem
rat.coe_int_neg
deleted
theorem
rat.coe_int_one
deleted
theorem
rat.coe_int_sub
deleted
theorem
rat.coe_nat_rat_eq_mk
added
theorem
rat.denom_dvd
added
theorem
rat.mk_eq_div
added
theorem
rat.mul_cast_comm
added
theorem
rat.num_dvd
added
theorem
rat.of_int_eq_mk
Modified
data/set/enumerate.lean
Deleted
meta/expr.lean