Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2017-07-24 00:42
aa78466d
View on Github →
refactor(*): move in some nat lemmas and other lemmas from init
Estimated changes
Created
data/array/lemmas.lean
added
theorem
array.mem_iff_list_mem
added
theorem
array.mem_iff_rev_list_mem
added
theorem
array.mem_iff_rev_list_mem_core
added
theorem
array.push_back_rev_list
added
theorem
array.push_back_rev_list_core
added
theorem
array.push_back_to_list
added
def
array.read_foreach
added
def
array.read_foreach_aux
added
def
array.read_map
added
def
array.read_map₂
added
theorem
array.read_write
added
theorem
array.read_write_eq
added
theorem
array.read_write_ne
added
theorem
array.rev_list_length
added
theorem
array.rev_list_length_aux
added
theorem
array.rev_list_reverse
added
theorem
array.rev_list_reverse_core
added
theorem
array.to_array_to_list
added
theorem
array.to_list_length
added
theorem
array.to_list_nth
added
theorem
array.to_list_nth_core
added
theorem
array.to_list_reverse
added
theorem
array.to_list_to_array
Modified
data/bitvec.lean
Modified
data/fin.lean
deleted
theorem
lt_succ_of_lt
Modified
data/hash_map.lean
Modified
data/int/basic.lean
added
theorem
int.abs_div_le_abs
added
theorem
int.add_mod_eq_add_mod_left
added
theorem
int.add_mod_eq_add_mod_right
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
added
theorem
int.add_mul_mod_self_left
added
theorem
int.bit0_val
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_bit
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.coe_nat_dvd_coe_nat_iff
added
theorem
int.coe_nat_dvd_coe_nat_of_dvd
added
theorem
int.div2_bit
added
theorem
int.div2_val
added
theorem
int.div_dvd_div
added
theorem
int.div_eq_div_of_mul_eq_mul
added
theorem
int.div_eq_zero_of_lt
added
theorem
int.div_eq_zero_of_lt_abs
added
theorem
int.div_le_self
added
theorem
int.div_mul_cancel_of_mod_eq_zero
added
theorem
int.div_neg'
added
theorem
int.div_of_neg_of_pos
added
theorem
int.div_pos_of_pos_of_dvd
added
theorem
int.dvd_antisymm
added
theorem
int.dvd_iff_mod_eq_zero
added
theorem
int.dvd_of_coe_nat_dvd_coe_nat
added
theorem
int.dvd_of_mod_eq_zero
added
theorem
int.eq_one_of_dvd_one
added
theorem
int.eq_one_of_mul_eq_one_left
added
theorem
int.eq_one_of_mul_eq_one_right
added
theorem
int.land_bit
added
theorem
int.ldiff_bit
added
theorem
int.le_of_dvd
added
theorem
int.lnot_bit
added
theorem
int.lor_bit
added
theorem
int.lt_div_add_one_mul_self
added
theorem
int.lxor_bit
added
theorem
int.mod_abs
added
theorem
int.mod_add_div
added
theorem
int.mod_add_div_aux
added
theorem
int.mod_add_mod
added
theorem
int.mod_def
added
theorem
int.mod_eq_mod_of_add_mod_eq_add_mod_left
added
theorem
int.mod_eq_mod_of_add_mod_eq_add_mod_right
added
theorem
int.mod_eq_of_lt
added
theorem
int.mod_eq_zero_of_dvd
added
theorem
int.mod_lt
added
theorem
int.mod_lt_of_pos
added
theorem
int.mod_neg
added
theorem
int.mod_nonneg
added
theorem
int.mod_one
added
theorem
int.mod_self
added
theorem
int.mod_zero
added
theorem
int.mul_div_cancel_of_mod_eq_zero
added
theorem
int.mul_div_mul_of_pos
added
theorem
int.mul_div_mul_of_pos_left
added
theorem
int.mul_mod_left
added
theorem
int.mul_mod_mul_of_pos
added
theorem
int.mul_mod_right
added
theorem
int.neg_div_of_dvd
added
theorem
int.neg_succ_of_nat_div
added
theorem
int.neg_succ_of_nat_mod
added
theorem
int.of_nat_div
added
theorem
int.of_nat_mod
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_mod
added
theorem
int.zero_shiftl
added
theorem
int.zero_shiftr
added
def
int.{u}
deleted
def
nat_succ_eq_int_succ
deleted
theorem
neg_nat_succ
deleted
theorem
neg_pred
deleted
theorem
neg_succ
deleted
theorem
neg_succ_of_nat_eq'
deleted
theorem
of_nat_sub
deleted
def
pred
deleted
theorem
pred_nat_succ
deleted
theorem
pred_neg_pred
deleted
theorem
pred_succ
deleted
def
rec_nat_on
deleted
theorem
rec_nat_on_neg
deleted
def
succ
deleted
theorem
succ_neg_nat_succ
deleted
theorem
succ_neg_succ
deleted
theorem
succ_pred
Modified
data/int/order.lean
added
theorem
int.exists_greatest_of_bdd
added
theorem
int.exists_least_of_bdd
Modified
data/list/basic.lean
added
theorem
list.app_subset_of_subset_of_subset
deleted
theorem
list.append.assoc
added
theorem
list.append_foldl
added
theorem
list.append_foldr
added
theorem
list.append_inj
added
theorem
list.append_inj_left
added
theorem
list.append_inj_right
added
theorem
list.append_ne_nil_of_ne_nil_left
added
theorem
list.append_ne_nil_of_ne_nil_right
added
theorem
list.append_right_inj
added
theorem
list.concat_eq_reverse_cons
added
theorem
list.cons_head_tail
modified
theorem
list.cons_ne_nil
added
theorem
list.cons_sublist_cons
added
theorem
list.cons_subset_of_subset_of_mem
added
theorem
list.eq_nil_of_forall_not_mem
added
theorem
list.eq_nil_of_infix_nil
added
theorem
list.eq_nil_of_length_eq_zero
added
theorem
list.eq_nil_of_map_eq_nil
added
theorem
list.eq_nil_of_prefix_nil
added
theorem
list.eq_nil_of_sublist_nil
added
theorem
list.eq_nil_of_subset_nil
added
theorem
list.eq_nil_of_suffix_nil
added
theorem
list.eq_of_map_const
added
theorem
list.exists_of_mem_bind
added
theorem
list.exists_of_mem_join
added
theorem
list.exists_of_mem_map
added
theorem
list.ext
added
theorem
list.ext_le
added
theorem
list.filter_subset
added
theorem
list.foldl_hom
added
theorem
list.foldl_map
added
theorem
list.foldr_eta
added
theorem
list.foldr_hom
added
theorem
list.foldr_map
added
theorem
list.head_append
added
theorem
list.infix_append
added
theorem
list.infix_iff_prefix_suffix
added
theorem
list.infix_of_prefix
added
theorem
list.infix_of_suffix
added
theorem
list.infix_refl
modified
def
list.inth
deleted
theorem
list.inth_succ
deleted
theorem
list.inth_zero
deleted
def
list.ith
deleted
theorem
list.ith_succ
deleted
theorem
list.ith_zero
added
theorem
list.last_append
added
theorem
list.last_concat
added
theorem
list.last_cons
added
theorem
list.length_le_of_infix
added
theorem
list.length_map₂
added
theorem
list.length_pos_of_mem
added
theorem
list.length_remove_nth
added
theorem
list.length_reverse
added
theorem
list.length_take
added
theorem
list.length_take_le
deleted
theorem
list.length_taken_le
added
theorem
list.map_id'
added
theorem
list.map_reverse
added
theorem
list.mem_append_of_mem_or_mem
added
theorem
list.mem_bind
added
theorem
list.mem_bind_iff
added
theorem
list.mem_filter_of_mem
added
theorem
list.mem_inits
added
theorem
list.mem_join
added
theorem
list.mem_join_iff
added
theorem
list.mem_map
added
theorem
list.mem_map_iff
added
theorem
list.mem_of_mem_cons_of_mem
added
theorem
list.mem_of_mem_filter
added
theorem
list.mem_of_ne_of_mem
added
theorem
list.mem_or_mem_of_mem_append
added
theorem
list.mem_reverse
added
theorem
list.mem_singleton
added
theorem
list.mem_singleton_iff
added
theorem
list.mem_split
added
theorem
list.mem_sublists
added
theorem
list.mem_tails
added
theorem
list.ne_and_not_mem_of_not_mem_cons
added
theorem
list.ne_nil_of_length_eq_succ
added
theorem
list.ne_of_not_mem_cons
added
theorem
list.nil_sublist
added
theorem
list.not_mem_append
added
theorem
list.not_mem_cons_of_ne_of_not_mem
added
theorem
list.not_mem_of_not_mem_append_left
added
theorem
list.not_mem_of_not_mem_append_right
added
theorem
list.not_mem_of_not_mem_cons
deleted
theorem
list.nth_eq_some
added
theorem
list.nth_ge_len
added
theorem
list.nth_le_nth
added
theorem
list.nth_le_reverse
added
theorem
list.nth_le_reverse_aux1
added
theorem
list.nth_le_reverse_aux2
added
theorem
list.of_mem_filter
added
theorem
list.prefix_append
added
theorem
list.prefix_refl
added
theorem
list.reverse_append
added
theorem
list.reverse_cons
added
theorem
list.reverse_nil
added
theorem
list.reverse_reverse
added
theorem
list.reverse_singleton
added
theorem
list.scanr_aux_cons
added
theorem
list.scanr_cons
added
theorem
list.scanr_nil
added
theorem
list.span_eq_take_drop
added
theorem
list.split_at_eq_take_drop
added
theorem
list.sublist.refl
added
theorem
list.sublist.trans
added
theorem
list.sublist_app_of_sublist_left
added
theorem
list.sublist_app_of_sublist_right
added
theorem
list.sublist_append_left
added
theorem
list.sublist_append_right
added
theorem
list.sublist_cons
added
theorem
list.sublist_cons_of_sublist
added
theorem
list.sublist_of_cons_sublist
added
theorem
list.sublist_of_cons_sublist_cons
added
theorem
list.sublist_of_infix
added
theorem
list.sublists_aux_cons_cons
added
theorem
list.sublists_aux_eq_foldl
added
theorem
list.subset_app_of_subset_left
added
theorem
list.subset_app_of_subset_right
added
theorem
list.subset_of_sublist
added
theorem
list.suffix_append
added
theorem
list.suffix_refl
added
theorem
list.take_all
added
theorem
list.take_all_of_ge
added
theorem
list.take_append_drop
added
theorem
list.take_cons
added
theorem
list.take_nil
added
theorem
list.take_take
added
theorem
list.take_while_append_drop
added
theorem
list.take_zero
deleted
theorem
list.taken_all
deleted
theorem
list.taken_all_of_ge
deleted
theorem
list.taken_cons
deleted
theorem
list.taken_nil
deleted
theorem
list.taken_zero
Modified
data/list/perm.lean
Modified
data/nat/basic.lean
deleted
def
iterate
added
theorem
nat.add_div_left
added
theorem
nat.add_div_right
added
theorem
nat.add_mod_left
added
theorem
nat.add_mod_right
added
theorem
nat.add_mul_div_left
added
theorem
nat.add_mul_div_right
added
theorem
nat.add_mul_mod_self_left
added
theorem
nat.add_mul_mod_self_right
deleted
theorem
nat.add_one
added
theorem
nat.binary_rec_eq
added
theorem
nat.bitwise_bit
added
theorem
nat.bitwise_bit_aux
added
theorem
nat.bitwise_swap
added
theorem
nat.bitwise_zero
added
theorem
nat.bitwise_zero_left
added
theorem
nat.bitwise_zero_right
added
theorem
nat.bodd_bit
added
theorem
nat.cond_to_bool_mod_two
modified
theorem
nat.discriminate
added
theorem
nat.div2_bit
added
theorem
nat.div_mul_le_self
added
theorem
nat.dvd_antisymm
added
theorem
nat.dvd_iff_mod_eq_zero
added
theorem
nat.dvd_mod_iff
added
theorem
nat.dvd_of_mod_eq_zero
added
theorem
nat.dvd_of_mul_dvd_mul_left
added
theorem
nat.dvd_of_mul_dvd_mul_right
added
theorem
nat.dvd_sub
added
theorem
nat.eq_one_of_dvd_one
added
theorem
nat.eq_zero_of_mul_eq_zero
added
def
nat.iterate
added
theorem
nat.land_bit
added
theorem
nat.ldiff_bit
added
theorem
nat.le_lt_antisymm
added
theorem
nat.le_mul_self
added
theorem
nat.le_of_dvd
added
theorem
nat.le_succ_of_pred_le
added
theorem
nat.lor_bit
added
theorem
nat.lt_le_antisymm
added
theorem
nat.lt_succ_of_lt
added
theorem
nat.lxor_bit
added
theorem
nat.min_succ_succ
added
theorem
nat.mod_eq_zero_of_dvd
added
theorem
nat.mod_le
added
theorem
nat.mod_pow_succ
added
theorem
nat.mul_div_left
added
theorem
nat.mul_div_right
added
theorem
nat.mul_mod_left
added
theorem
nat.mul_mod_mul_left
added
theorem
nat.mul_mod_mul_right
added
theorem
nat.mul_mod_right
added
theorem
nat.mul_pred_left
added
theorem
nat.mul_pred_right
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.mul_sub_div
added
def
nat.one_pos
added
theorem
nat.one_shiftl
added
theorem
nat.pos_of_dvd_of_pos
added
theorem
nat.pos_pow_of_pos
added
theorem
nat.pow_le_pow_of_le_left
added
theorem
nat.pow_le_pow_of_le_right
added
theorem
nat.pow_lt_pow_of_lt_left
added
theorem
nat.pow_lt_pow_of_lt_right
added
theorem
nat.pow_one
added
theorem
nat.pred_inj
added
theorem
nat.shiftl'_add
added
theorem
nat.shiftl'_sub
added
theorem
nat.shiftl'_tt_eq_mul_pow
added
theorem
nat.shiftl_add
added
theorem
nat.shiftl_eq_mul_pow
added
theorem
nat.shiftl_sub
added
theorem
nat.shiftr_add
added
theorem
nat.shiftr_eq_div_pow
added
theorem
nat.sub_add_min_cancel
added
theorem
nat.sub_eq_sub_min
added
theorem
nat.sub_mul_div
added
theorem
nat.sub_mul_mod
added
theorem
nat.sub_one_sub_lt
added
theorem
nat.succ_mul_succ_eq
added
theorem
nat.succ_sub
added
theorem
nat.succ_sub_sub_succ
added
theorem
nat.test_bit_bitwise
added
theorem
nat.test_bit_land
added
theorem
nat.test_bit_ldiff
added
theorem
nat.test_bit_lor
added
theorem
nat.test_bit_lxor
added
theorem
nat.test_bit_succ
added
theorem
nat.test_bit_zero
added
theorem
nat.zero_pow
added
theorem
nat.zero_shiftl
added
theorem
nat.zero_shiftr
Modified
data/nat/gcd.lean
Modified
data/nat/sub.lean
Created
data/option.lean
added
def
option.iget
Modified
data/seq/computation.lean
Modified
data/seq/wseq.lean
Modified
data/stream.lean