Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-28 18:34 4ed43d95

View on Github →

feat(data/finset): add fold; add simp rules for insert, empty, singleton and mem

Estimated changes

Modified algebra/big_operators.lean

modified theorem finset.prod_insert

deleted theorem finset.prod_to_finset

added theorem finset.prod_to_finset_of_nodup

added theorem finset.prod_union_inter

deleted theorem finset.prod_union_inter_eq

deleted theorem foldl_mul_assoc

deleted theorem foldl_mul_eq_mul_foldr

added theorem list.prod_append

added theorem list.prod_cons

added theorem list.prod_eq_of_perm

added theorem list.prod_join

added theorem list.prod_nil

added theorem list.prod_replicate

added theorem list.prod_reverse

deleted theorem prod_append

deleted theorem prod_cons

deleted theorem prod_eq_of_perm

deleted theorem prod_join

deleted theorem prod_nil

deleted theorem prod_replicate

Modified data/finset/basic.lean

modified theorem finset.card_empty

modified theorem finset.card_erase_of_mem

deleted theorem finset.card_erase_of_not_mem

modified theorem finset.card_insert_le

deleted theorem finset.card_insert_of_mem

modified theorem finset.card_insert_of_not_mem

modified theorem finset.card_upto

modified theorem finset.empty_inter

modified theorem finset.empty_subset

modified theorem finset.empty_union

modified theorem finset.eq_empty_of_card_eq_zero

modified theorem finset.eq_empty_of_forall_not_mem

modified theorem finset.eq_empty_of_subset_empty

modified theorem finset.eq_of_mem_singleton

modified theorem finset.eq_of_singleton_eq

deleted theorem finset.eq_of_subset_of_subset

deleted theorem finset.eq_or_mem_of_mem_insert

modified theorem finset.erase_empty

modified theorem finset.erase_eq_of_not_mem

modified theorem finset.erase_insert

modified theorem finset.erase_insert_subset

modified theorem finset.erase_subset

modified theorem finset.erase_subset_erase

modified theorem finset.erase_subset_of_subset_insert

modified theorem finset.exists_mem_of_ne_empty

modified theorem finset.forall_of_forall_insert

modified theorem finset.insert.comm

modified theorem finset.insert_eq

modified theorem finset.insert_eq_of_mem

modified theorem finset.insert_erase

modified theorem finset.insert_erase_subset

added theorem finset.insert_idem

modified theorem finset.insert_inter_of_mem

modified theorem finset.insert_inter_of_not_mem

added theorem finset.insert_ne_empty

added theorem finset.insert_singelton_self_eq

modified theorem finset.insert_subset_insert

modified theorem finset.insert_union

modified theorem finset.inter_assoc

modified theorem finset.inter_comm

modified theorem finset.inter_empty

added theorem finset.inter_insert_of_mem

added theorem finset.inter_insert_of_not_mem

modified theorem finset.inter_left_comm

modified theorem finset.inter_right_comm

modified theorem finset.inter_self

added theorem finset.inter_singleton_of_mem

added theorem finset.inter_singleton_of_not_mem

modified theorem finset.lt_of_mem_upto

modified theorem finset.mem_empty_iff

modified theorem finset.mem_erase_iff

modified theorem finset.mem_erase_of_ne_of_mem

modified theorem finset.mem_insert

modified theorem finset.mem_insert_iff

modified theorem finset.mem_insert_of_mem

modified theorem finset.mem_inter_iff

modified theorem finset.mem_of_mem_erase

modified theorem finset.mem_of_mem_insert_of_ne

modified theorem finset.mem_singleton

modified theorem finset.mem_singleton_iff

modified theorem finset.mem_singleton_of_eq

deleted theorem finset.mem_to_finset_of_nodup

added theorem finset.mem_to_finset_of_nodup_eq

modified theorem finset.mem_union_iff

deleted theorem finset.mem_union_l

deleted theorem finset.mem_union_r

modified theorem finset.mem_upto_iff

modified theorem finset.mem_upto_of_lt

modified theorem finset.mem_upto_succ_of_mem_upto

modified theorem finset.ne_empty_of_card_eq_succ

modified theorem finset.ne_of_mem_erase

modified theorem finset.not_mem_empty

modified theorem finset.not_mem_erase

deleted theorem finset.pair_eq_singleton

deleted theorem finset.perm_insert_cons_of_not_mem

modified theorem finset.singleton_inter_of_mem

modified theorem finset.singleton_inter_of_not_mem

modified theorem finset.singleton_ne_empty

modified theorem finset.subset_insert

modified theorem finset.subset_insert_of_erase_subset

modified theorem finset.union_assoc

modified theorem finset.union_comm

modified theorem finset.union_empty

added theorem finset.union_insert

modified theorem finset.union_self

modified def finset.upto

modified theorem finset.upto_succ

added theorem or_self_or

added theorem perm_insert_cons_of_not_mem

Created data/finset/default.lean

Created data/finset/fold.lean

added def finset.fold

added theorem finset.fold_empty

added theorem finset.fold_hom

added theorem finset.fold_image

added theorem finset.fold_insert

added theorem finset.fold_op_distrib

added theorem finset.fold_singleton

added theorem finset.fold_to_finset_of_nodup

added theorem finset.fold_union_inter

added theorem list.fold_op_eq_of_perm

added theorem list.foldl_assoc

added theorem list.foldl_assoc_comm_cons

added theorem list.foldl_op_eq_op_foldr_assoc

Modified data/list/set.lean

added theorem list.mem_erase_iff_of_nodup

modified theorem list.mem_erase_of_nodup