Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-01 04:35 0663945f

View on Github →

feat(data/num,data/multiset): more properties of binary numbers, begin multisets

Estimated changes

Modified algebra/field.lean

added theorem division_ring.inv_div

added theorem division_ring.inv_inv

added theorem division_ring.one_div_div

added theorem inv_ne_zero

Modified algebra/group_power.lean

added theorem has_pow_nat_eq_pow_nat

added theorem pow_bit0

added theorem pow_bit1

Modified algebra/ordered_group.lean

added theorem bit0_pos

Modified algebra/ordered_ring.lean

added theorem bit1_pos'

added theorem bit1_pos

Modified data/int/basic.lean

added theorem int.cast_coe_nat'

Created data/multiset/basic.lean

added theorem multiset.add_cons

added theorem multiset.add_sub_of_le

added def multiset.card

added theorem multiset.card_add

added theorem multiset.card_cons

added theorem multiset.card_empty

added theorem multiset.card_erase_of_mem

added theorem multiset.card_insert_le

added theorem multiset.card_insert_of_not_mem

added theorem multiset.card_le_of_le

added theorem multiset.card_lt_of_lt

added theorem multiset.card_range

added theorem multiset.card_zero

added theorem multiset.coe_add

added theorem multiset.coe_card

added theorem multiset.coe_eq_coe

added theorem multiset.coe_erase

added theorem multiset.coe_foldl

added theorem multiset.coe_foldr

added theorem multiset.coe_foldr_swap

added theorem multiset.coe_join

added theorem multiset.coe_le

added theorem multiset.coe_nil_eq_zero

added theorem multiset.coe_reverse

added theorem multiset.coe_sub

added def multiset.cons

added theorem multiset.cons_coe

added theorem multiset.cons_inj_left

added theorem multiset.cons_inj_right

added theorem multiset.cons_le_cons

added theorem multiset.cons_le_cons_iff

added theorem multiset.cons_swap

added theorem multiset.empty_inter

added theorem multiset.empty_subset

added theorem multiset.eq_cons_erase

added theorem multiset.eq_empty_of_card_eq_zero

added theorem multiset.eq_empty_of_forall_not_mem

added theorem multiset.eq_empty_of_subset_empty

added theorem multiset.eq_of_le_of_card_le

added theorem multiset.eq_zero_of_le_zero

added def multiset.erase

added theorem multiset.erase_add_left_neg

added theorem multiset.erase_add_left_pos

added theorem multiset.erase_add_right_neg

added theorem multiset.erase_add_right_pos

added theorem multiset.erase_comm

added theorem multiset.erase_cons_head

added theorem multiset.erase_cons_tail

added theorem multiset.erase_dup_map_erase_dup_eq

added theorem multiset.erase_empty

added theorem multiset.erase_eq_of_not_mem

added theorem multiset.erase_insert

added theorem multiset.erase_insert_subset

added theorem multiset.erase_le

added theorem multiset.erase_of_not_mem

added theorem multiset.erase_subset

added theorem multiset.erase_subset_erase

added theorem multiset.erase_subset_of_subset_insert

added theorem multiset.erase_zero

added theorem multiset.exists_cons_of_mem

added theorem multiset.exists_mem_empty_iff

added theorem multiset.exists_mem_insert

added theorem multiset.exists_mem_of_ne_empty

added theorem multiset.exists_nat_subset_range

added theorem multiset.filter_false

added theorem multiset.filter_filter

added theorem multiset.filter_inter_filter_neg_eq

added theorem multiset.filter_subset

added theorem multiset.filter_union

added theorem multiset.filter_union_filter_neg_eq

added def multiset.foldl

added theorem multiset.foldl_swap

added def multiset.foldr

added theorem multiset.foldr_swap

added theorem multiset.forall_mem_empty_iff

added theorem multiset.forall_mem_insert

added theorem multiset.image_empty

added theorem multiset.image_eq_empty_iff

added theorem multiset.image_filter

added theorem multiset.image_id

added theorem multiset.image_image

added theorem multiset.image_insert

added theorem multiset.image_inter

added theorem multiset.image_singleton

added theorem multiset.image_subset_image

added theorem multiset.image_to_multiset

added theorem multiset.image_to_multiset_of_nodup

added theorem multiset.image_union

added theorem multiset.insert_erase

added theorem multiset.insert_erase_subset

added theorem multiset.insert_inter_of_mem

added theorem multiset.insert_inter_of_not_mem

added theorem multiset.inter_assoc

added theorem multiset.inter_comm

added theorem multiset.inter_distrib_left

added theorem multiset.inter_distrib_right

added theorem multiset.inter_empty

added theorem multiset.inter_insert_of_mem

added theorem multiset.inter_insert_of_not_mem

added theorem multiset.inter_left_comm

added theorem multiset.inter_right_comm

added theorem multiset.inter_self

added theorem multiset.inter_singleton_of_mem

added theorem multiset.inter_singleton_of_not_mem

added theorem multiset.inter_subset_left

added theorem multiset.inter_subset_right

added def multiset.join

added theorem multiset.le_add_left

added theorem multiset.le_add_right

added theorem multiset.le_cons_self

added theorem multiset.le_iff_exists_add

added theorem multiset.le_induction_on

added theorem multiset.lt_cons_self

added theorem multiset.lt_iff_cons_le

added def multiset.map

added def multiset.mem

added theorem multiset.mem_coe

added theorem multiset.mem_cons

added theorem multiset.mem_cons_self

added theorem multiset.mem_erase

added theorem multiset.mem_erase_of_ne_of_mem

added theorem multiset.mem_filter

added theorem multiset.mem_image_iff

added theorem multiset.mem_inter

added theorem multiset.mem_inter_of_mem

added theorem multiset.mem_map

added theorem multiset.mem_map_of_inj

added theorem multiset.mem_map_of_mem

added theorem multiset.mem_of_le

added theorem multiset.mem_of_mem_erase

added theorem multiset.mem_of_mem_inter_left

added theorem multiset.mem_of_mem_inter_right

added theorem multiset.mem_of_subset

added theorem multiset.mem_range

added theorem multiset.mem_sdiff_iff

added theorem multiset.mem_singleton

added theorem multiset.mem_singleton_self

added theorem multiset.ne_empty_of_card_eq_succ

added theorem multiset.ne_of_mem_erase

added theorem multiset.not_mem_empty

added theorem multiset.not_mem_erase

added theorem multiset.not_mem_range_self

added def multiset.prod

added def multiset.prod_eq_foldl

added def multiset.prod_eq_foldr

added theorem multiset.quot_mk_to_coe'

added theorem multiset.quot_mk_to_coe

added def multiset.range

added theorem multiset.range_subset

added theorem multiset.range_succ

added theorem multiset.range_zero

added theorem multiset.sdiff_inter_self

added theorem multiset.sdiff_subset_sdiff

added theorem multiset.sdiff_union_of_subset

added theorem multiset.singleton_add

added theorem multiset.singleton_coe

added theorem multiset.singleton_inj

added theorem multiset.singleton_inter_of_mem

added theorem multiset.singleton_inter_of_not_mem

added theorem multiset.singleton_ne_zero

added theorem multiset.sub_add_cancel

added theorem multiset.sub_cons

added theorem multiset.sub_eq_fold_erase

added theorem multiset.sub_zero

added theorem multiset.subset.refl

added theorem multiset.subset.trans

added theorem multiset.subset_empty_iff

added theorem multiset.subset_iff

added theorem multiset.subset_insert_iff

added theorem multiset.subset_insert_of_erase_subset

added theorem multiset.subset_inter

added theorem multiset.subset_of_le

added def multiset.sum

added theorem multiset.union_distrib_left

added theorem multiset.union_distrib_right

added theorem multiset.zero_le

added def {u}

Modified data/nat/basic.lean

added def nat.ppred

added theorem nat.ppred_eq_none

added theorem nat.ppred_eq_pred

added theorem nat.ppred_eq_some

added theorem nat.pred_eq_ppred

added def nat.psub

added theorem nat.psub_add

added theorem nat.psub_eq_none

added theorem nat.psub_eq_some

added theorem nat.psub_eq_sub

added theorem nat.size_one

added theorem nat.sub_eq_psub

Modified data/nat/cast.lean

modified theorem nat.cast_bit0

modified theorem nat.cast_bit1

Modified data/num/basic.lean

deleted def num.of_nat

added def num.of_znum'

added def num.of_znum

added def num.ppred

added def num.psub

added def num.sub'

added def num.to_znum_neg

added def pos_num.of_znum'

added def pos_num.of_znum

modified def pos_num.pred'

modified def pos_num.pred

deleted def pos_num.psub

added def pos_num.sub'

Modified data/num/lemmas.lean

modified theorem num.add_of_nat

added theorem num.add_one

added theorem num.add_to_nat

added theorem num.add_to_znum

added theorem num.bit0_of_bit0

added theorem num.bit1_of_bit1

deleted theorem num.cast_add

deleted theorem num.cast_cmp'

deleted theorem num.cast_cmp

modified theorem num.cast_one

added theorem num.cast_sub'

modified theorem num.cast_succ'

added theorem num.cast_to_int

added theorem num.cast_to_nat

added theorem num.cast_to_znum

added theorem num.cast_to_znum_neg

modified theorem num.cast_zero

added theorem num.cmp_to_nat

added theorem num.le_to_nat

added theorem num.lt_to_nat

added theorem num.mul_to_nat

modified theorem num.of_nat_inj

added theorem num.of_nat_to_znum

added theorem num.of_nat_to_znum_neg

added theorem num.ppred_to_nat

added theorem num.succ'_to_nat

added theorem num.succ_to_nat

modified theorem num.to_nat_inj

added theorem num.zneg_to_znum

added theorem num.zneg_to_znum_neg

added theorem pos_num.add_to_nat

modified theorem pos_num.cast_add

deleted theorem pos_num.cast_add_comm

deleted theorem pos_num.cast_add_comm_lemma_1

deleted theorem pos_num.cast_add_comm_lemma_2

deleted theorem pos_num.cast_add_one_comm

added theorem pos_num.cast_bit0

added theorem pos_num.cast_bit1

deleted theorem pos_num.cast_cmp'

deleted theorem pos_num.cast_cmp

modified theorem pos_num.cast_mul

modified theorem pos_num.cast_one

added theorem pos_num.cast_sub'

modified theorem pos_num.cast_succ

added theorem pos_num.cast_to_int

added theorem pos_num.cast_to_nat

added theorem pos_num.cast_to_num

added theorem pos_num.cast_to_znum

added theorem pos_num.cmp_to_nat

added theorem pos_num.cmp_to_nat_lemma

added theorem pos_num.le_to_nat

added theorem pos_num.lt_to_nat

added theorem pos_num.mul_to_nat

modified theorem pos_num.of_to_nat

deleted theorem pos_num.one_add

modified theorem pos_num.one_le_cast

added theorem pos_num.one_sub'

added theorem pos_num.pred'_succ'

modified theorem pos_num.pred'_to_nat

added theorem pos_num.size_to_nat

added theorem pos_num.sub'_one

added theorem pos_num.succ'_pred'

added theorem pos_num.succ_to_nat

modified theorem pos_num.to_nat_inj

added theorem pos_num.to_nat_pos

added theorem znum.add_of_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_neg

modified theorem znum.cast_one

added theorem znum.cast_pos

added theorem znum.cast_to_int

modified theorem znum.cast_zero

added theorem znum.cast_zneg

added theorem znum.neg_of_int

added theorem znum.neg_zero

added theorem znum.of_to_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

Modified data/option.lean

deleted theorem option.bind_none

modified theorem option.bind_some

added theorem option.none_bind

added theorem option.some_bind

Modified data/rat.lean

added theorem rat.cast_div

added theorem rat.cast_div_of_ne_zero

added theorem rat.cast_inv

added theorem rat.cast_inv_of_ne_zero

Modified data/seq/seq.lean