Commit 2023-01-13 09:59 1f3f3d7b

View on Github →

feat: port Data.Multiset.Basic (#1491)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Perm.lean

added theorem List.Perm.bagInter

added theorem List.Perm.bagInter_left

added theorem List.Perm.bagInter_right

deleted theorem List.Perm.bag_inter

deleted theorem List.Perm.bag_inter_left

deleted theorem List.Perm.bag_inter_right

modified theorem List.Perm.countp_congr

modified theorem List.Perm.countp_eq

modified theorem List.Perm.filter

modified theorem List.Subperm.countp_le

modified theorem List.Subperm.filter

modified theorem List.countp_eq_countp_filter_add

modified theorem List.filter_append_perm

Modified Mathlib/Data/Multiset/Basic.lean

added theorem Multiset.Disjoint.symm

added def Multiset.Disjoint

added def Multiset.Pairwise

added theorem Multiset.Rel.add

added theorem Multiset.Rel.countp_eq

added theorem Multiset.Rel.mono

added theorem Multiset.Rel.trans

added inductive Multiset.Rel

added theorem Multiset.Subset.refl

added theorem Multiset.Subset.trans

added theorem Multiset.addHom_ext

added theorem Multiset.add_cons

added theorem Multiset.add_eq_union_iff_disjoint

added theorem Multiset.add_inter_distrib

added theorem Multiset.add_singleton_eq_iff

added theorem Multiset.add_union_distrib

added def Multiset.attach

added theorem Multiset.attach_cons

added theorem Multiset.attach_count_eq_count_coe

added theorem Multiset.attach_map_val'

added theorem Multiset.attach_map_val

added theorem Multiset.attach_zero

added theorem Multiset.bot_eq_zero

added def Multiset.card

added theorem Multiset.card_add

added theorem Multiset.card_attach

added theorem Multiset.card_cons

added theorem Multiset.card_eq_card_of_rel

added theorem Multiset.card_eq_countp_add_countp

added theorem Multiset.card_eq_one

added theorem Multiset.card_eq_three

added theorem Multiset.card_eq_two

added theorem Multiset.card_eq_zero

added theorem Multiset.card_erase_add_one

added theorem Multiset.card_erase_eq_ite

added theorem Multiset.card_erase_le

added theorem Multiset.card_erase_lt_of_mem

added theorem Multiset.card_erase_of_mem

added theorem Multiset.card_le_of_le

added theorem Multiset.card_lt_of_lt

added theorem Multiset.card_map

added theorem Multiset.card_mono

added theorem Multiset.card_nsmul

added theorem Multiset.card_pair

added theorem Multiset.card_pmap

added theorem Multiset.card_pos

added theorem Multiset.card_pos_iff_exists_mem

added theorem Multiset.card_repeat

added theorem Multiset.card_singleton

added theorem Multiset.card_sub

added theorem Multiset.card_zero

added theorem Multiset.case_strongInductionOn

added def Multiset.choose

added def Multiset.chooseX

added theorem Multiset.choose_mem

added theorem Multiset.choose_property

added theorem Multiset.choose_spec

added theorem Multiset.coe_add

added theorem Multiset.coe_attach

added theorem Multiset.coe_card

added theorem Multiset.coe_count

added theorem Multiset.coe_countAddMonoidHom

added theorem Multiset.coe_countp

added theorem Multiset.coe_countpAddMonoidHom

added theorem Multiset.coe_disjoint

added theorem Multiset.coe_eq_coe

added theorem Multiset.coe_eq_zero

added theorem Multiset.coe_eq_zero_iff_isEmpty

added theorem Multiset.coe_erase

added theorem Multiset.coe_filter

added theorem Multiset.coe_filterMap

added theorem Multiset.coe_foldl

added theorem Multiset.coe_foldr

added theorem Multiset.coe_foldr_swap

added theorem Multiset.coe_inter

added theorem Multiset.coe_le

added theorem Multiset.coe_map

added theorem Multiset.coe_mapAddMonoidHom

added theorem Multiset.coe_nil

added theorem Multiset.coe_pmap

added theorem Multiset.coe_repeat

added theorem Multiset.coe_reverse

added theorem Multiset.coe_singleton

added theorem Multiset.coe_sub

added theorem Multiset.coe_subset

added theorem Multiset.coe_subsingletonEquiv

added theorem Multiset.coe_toList

added def Multiset.cons

added theorem Multiset.cons_add

added theorem Multiset.cons_coe

added theorem Multiset.cons_eq_cons

added theorem Multiset.cons_erase

added theorem Multiset.cons_inj_left

added theorem Multiset.cons_inj_right

added theorem Multiset.cons_inter_distrib

added theorem Multiset.cons_inter_of_neg

added theorem Multiset.cons_inter_of_pos

added theorem Multiset.cons_le_cons

added theorem Multiset.cons_le_cons_iff

added theorem Multiset.cons_ne_zero

added theorem Multiset.cons_sub_of_le

added theorem Multiset.cons_subset

added theorem Multiset.cons_subset_cons

added theorem Multiset.cons_swap

added theorem Multiset.cons_union_distrib

added theorem Multiset.cons_zero

added def Multiset.count

added def Multiset.countAddMonoidHom

added theorem Multiset.count_add

added theorem Multiset.count_cons

added theorem Multiset.count_cons_of_ne

added theorem Multiset.count_cons_self

added theorem Multiset.count_eq_card

added theorem Multiset.count_eq_card_filter_eq

added theorem Multiset.count_eq_zero

added theorem Multiset.count_eq_zero_of_not_mem

added theorem Multiset.count_erase_of_ne

added theorem Multiset.count_erase_self

added theorem Multiset.count_filter

added theorem Multiset.count_filter_of_neg

added theorem Multiset.count_filter_of_pos

added theorem Multiset.count_inter

added theorem Multiset.count_le_card

added theorem Multiset.count_le_count_cons

added theorem Multiset.count_le_of_le

added theorem Multiset.count_map

added theorem Multiset.count_map_eq_count'

added theorem Multiset.count_map_eq_count

added theorem Multiset.count_ne_zero

added theorem Multiset.count_nsmul

added theorem Multiset.count_pos

added theorem Multiset.count_repeat

added theorem Multiset.count_repeat_self

added theorem Multiset.count_singleton

added theorem Multiset.count_singleton_self

added theorem Multiset.count_sub

added theorem Multiset.count_union

added theorem Multiset.count_zero

added def Multiset.countp

added def Multiset.countpAddMonoidHom

added theorem Multiset.countp_add

added theorem Multiset.countp_congr

added theorem Multiset.countp_cons

added theorem Multiset.countp_cons_of_neg

added theorem Multiset.countp_cons_of_pos

added theorem Multiset.countp_eq_card

added theorem Multiset.countp_eq_card_filter

added theorem Multiset.countp_eq_countp_filter_add

added theorem Multiset.countp_eq_zero

added theorem Multiset.countp_false

added theorem Multiset.countp_filter

added theorem Multiset.countp_le_card

added theorem Multiset.countp_le_of_le

added theorem Multiset.countp_map

added theorem Multiset.countp_nsmul

added theorem Multiset.countp_pos

added theorem Multiset.countp_pos_of_mem

added theorem Multiset.countp_sub

added theorem Multiset.countp_true

added theorem Multiset.countp_zero

added theorem Multiset.disjoint_add_left

added theorem Multiset.disjoint_add_right

added theorem Multiset.disjoint_comm

added theorem Multiset.disjoint_cons_left

added theorem Multiset.disjoint_cons_right

added theorem Multiset.disjoint_iff_ne

added theorem Multiset.disjoint_left

added theorem Multiset.disjoint_map_map

added theorem Multiset.disjoint_of_le_left

added theorem Multiset.disjoint_of_le_right

added theorem Multiset.disjoint_of_subset_left

added theorem Multiset.disjoint_of_subset_right

added theorem Multiset.disjoint_right

added theorem Multiset.disjoint_singleton

added theorem Multiset.disjoint_union_left

added theorem Multiset.disjoint_union_right

added theorem Multiset.empty_eq_zero

added theorem Multiset.empty_or_exists_mem

added theorem Multiset.empty_toList

added theorem Multiset.eq_of_le_of_card_le

added theorem Multiset.eq_of_mem_map_const

added theorem Multiset.eq_of_mem_repeat

added theorem Multiset.eq_repeat'

added theorem Multiset.eq_repeat

added theorem Multiset.eq_repeat_of_mem

added theorem Multiset.eq_union_left

added theorem Multiset.eq_union_right

added theorem Multiset.eq_zero_iff_forall_not_mem

added theorem Multiset.eq_zero_of_forall_not_mem

added theorem Multiset.eq_zero_of_subset_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_le

added theorem Multiset.erase_le_erase

added theorem Multiset.erase_le_iff_le_cons

added theorem Multiset.erase_lt

added theorem Multiset.erase_of_not_mem

added theorem Multiset.erase_singleton

added theorem Multiset.erase_subset

added theorem Multiset.erase_zero

added theorem Multiset.exists_cons_of_mem

added theorem Multiset.exists_mem_of_ne_zero

added theorem Multiset.exists_mem_of_rel_of_mem

added theorem Multiset.exists_multiset_eq_map_quot_mk

added theorem Multiset.ext'

added theorem Multiset.ext

added def Multiset.filter

added def Multiset.filterMap

added theorem Multiset.filterMap_cons_none

added theorem Multiset.filterMap_cons_some

added theorem Multiset.filterMap_eq_filter

added theorem Multiset.filterMap_eq_map

added theorem Multiset.filterMap_filter

added theorem Multiset.filterMap_filterMap

added theorem Multiset.filterMap_le_filterMap

added theorem Multiset.filterMap_map

added theorem Multiset.filterMap_some

added theorem Multiset.filterMap_zero

added theorem Multiset.filter_add

added theorem Multiset.filter_add_filter

added theorem Multiset.filter_add_not

added theorem Multiset.filter_congr

added theorem Multiset.filter_cons

added theorem Multiset.filter_cons_of_neg

added theorem Multiset.filter_cons_of_pos

added theorem Multiset.filter_eq'

added theorem Multiset.filter_eq

added theorem Multiset.filter_eq_nil

added theorem Multiset.filter_eq_self

added theorem Multiset.filter_filter

added theorem Multiset.filter_filterMap

added theorem Multiset.filter_inter

added theorem Multiset.filter_le

added theorem Multiset.filter_le_filter

added theorem Multiset.filter_nsmul

added theorem Multiset.filter_singleton

added theorem Multiset.filter_sub

added theorem Multiset.filter_subset

added theorem Multiset.filter_union

added theorem Multiset.filter_zero

added def Multiset.foldl

added theorem Multiset.foldl_add

added theorem Multiset.foldl_cons

added theorem Multiset.foldl_induction'

added theorem Multiset.foldl_induction

added theorem Multiset.foldl_swap

added theorem Multiset.foldl_zero

added def Multiset.foldr

added theorem Multiset.foldr_add

added theorem Multiset.foldr_cons

added theorem Multiset.foldr_induction'

added theorem Multiset.foldr_induction

added theorem Multiset.foldr_singleton

added theorem Multiset.foldr_swap

added theorem Multiset.foldr_zero

added theorem Multiset.forall_mem_cons

added theorem Multiset.forall_mem_map_iff

added theorem Multiset.induction_on'

added theorem Multiset.induction_on_multiset_quot

added theorem Multiset.inf_eq_inter

added theorem Multiset.insert_eq_cons

added def Multiset.inter

added theorem Multiset.inter_add_distrib

added theorem Multiset.inter_comm

added theorem Multiset.inter_eq_zero_iff_disjoint

added theorem Multiset.inter_le_left

added theorem Multiset.inter_le_right

added theorem Multiset.inter_repeat

added theorem Multiset.inter_zero

added theorem Multiset.leInductionOn

added theorem Multiset.le_add_left

added theorem Multiset.le_add_right

added theorem Multiset.le_cons_erase

added theorem Multiset.le_cons_of_not_mem

added theorem Multiset.le_cons_self

added theorem Multiset.le_count_iff_repeat_le

added theorem Multiset.le_filter

added theorem Multiset.le_iff_count

added theorem Multiset.le_iff_exists_add

added theorem Multiset.le_inter

added theorem Multiset.le_inter_iff

added theorem Multiset.le_repeat_iff

added theorem Multiset.le_union_left

added theorem Multiset.le_union_right

added theorem Multiset.le_zero

added theorem Multiset.length_toList

added theorem Multiset.lt_cons_self

added theorem Multiset.lt_iff_cons_le

added theorem Multiset.lt_repeat_succ

added def Multiset.map

added def Multiset.mapAddMonoidHom

added def Multiset.mapEmbedding

added theorem Multiset.map_add

added theorem Multiset.map_comp_cons

added theorem Multiset.map_congr

added theorem Multiset.map_cons

added theorem Multiset.map_const'

added theorem Multiset.map_const

added theorem Multiset.map_count_true_eq_filter_card

added theorem Multiset.map_eq_cons

added theorem Multiset.map_eq_map

added theorem Multiset.map_eq_singleton

added theorem Multiset.map_eq_zero

added theorem Multiset.map_erase

added theorem Multiset.map_filter

added theorem Multiset.map_filterMap

added theorem Multiset.map_filterMap_of_inv

added theorem Multiset.map_hcongr

added theorem Multiset.map_id'

added theorem Multiset.map_id

added theorem Multiset.map_injective

added theorem Multiset.map_le_map

added theorem Multiset.map_le_map_iff

added theorem Multiset.map_lt_map

added theorem Multiset.map_map

added theorem Multiset.map_mk_eq_map_mk_of_rel

added theorem Multiset.map_mono

added theorem Multiset.map_nsmul

added theorem Multiset.map_pmap

added theorem Multiset.map_repeat

added theorem Multiset.map_set_pairwise

added theorem Multiset.map_singleton

added theorem Multiset.map_strictMono

added theorem Multiset.map_subset_map

added theorem Multiset.map_surjective_of_surjective

added theorem Multiset.map_union

added theorem Multiset.map_zero

added theorem Multiset.mem_add

added theorem Multiset.mem_attach

added theorem Multiset.mem_coe

added theorem Multiset.mem_cons

added theorem Multiset.mem_cons_of_mem

added theorem Multiset.mem_cons_self

added theorem Multiset.mem_erase_of_ne

added theorem Multiset.mem_filter

added theorem Multiset.mem_filterMap

added theorem Multiset.mem_filter_of_mem

added theorem Multiset.mem_inter

added theorem Multiset.mem_map

added theorem Multiset.mem_map_of_injective

added theorem Multiset.mem_map_of_mem

added theorem Multiset.mem_nsmul

added theorem Multiset.mem_of_le

added theorem Multiset.mem_of_mem_erase

added theorem Multiset.mem_of_mem_filter

added theorem Multiset.mem_of_mem_nsmul

added theorem Multiset.mem_of_subset

added theorem Multiset.mem_pmap

added theorem Multiset.mem_repeat

added theorem Multiset.mem_singleton

added theorem Multiset.mem_singleton_self

added theorem Multiset.mem_toList

added theorem Multiset.mem_union

added theorem Multiset.monotone_filter_left

added theorem Multiset.monotone_filter_right

added theorem Multiset.not_mem_mono

added theorem Multiset.not_mem_zero

added theorem Multiset.nsmul_cons

added theorem Multiset.nsmul_repeat

added theorem Multiset.nsmul_singleton

added def Multiset.ofList

added theorem Multiset.of_mem_filter

added theorem Multiset.one_le_count_iff_mem

added theorem Multiset.pair_comm

added theorem Multiset.pairwise_coe_iff

added theorem Multiset.pairwise_coe_iff_pairwise

added theorem Multiset.pairwise_nil

added theorem Multiset.pmap_congr

added theorem Multiset.pmap_cons

added theorem Multiset.pmap_eq_map

added theorem Multiset.pmap_eq_map_attach

added theorem Multiset.pmap_zero

added theorem Multiset.quot_mk_to_coe''

added theorem Multiset.quot_mk_to_coe'

added theorem Multiset.quot_mk_to_coe

added def Multiset.rec

added def Multiset.recOn

added theorem Multiset.recOn_0

added theorem Multiset.recOn_cons

added theorem Multiset.rel_add_left

added theorem Multiset.rel_add_right

added theorem Multiset.rel_cons_left

added theorem Multiset.rel_cons_right

added theorem Multiset.rel_eq

added theorem Multiset.rel_eq_refl

added theorem Multiset.rel_flip

added theorem Multiset.rel_flip_eq

added theorem Multiset.rel_map

added theorem Multiset.rel_map_left

added theorem Multiset.rel_map_right

added theorem Multiset.rel_of_forall

added theorem Multiset.rel_refl_of_refl_on

added theorem Multiset.rel_repeat_left

added theorem Multiset.rel_repeat_right

added theorem Multiset.rel_zero_left

added theorem Multiset.rel_zero_right

added def Multiset.repeatAddMonoidHom

added theorem Multiset.repeat_add

added theorem Multiset.repeat_inf

added theorem Multiset.repeat_injective

added theorem Multiset.repeat_inter

added theorem Multiset.repeat_le_coe

added theorem Multiset.repeat_le_repeat

added theorem Multiset.repeat_left_inj

added theorem Multiset.repeat_left_injective

added theorem Multiset.repeat_one

added theorem Multiset.repeat_subset_singleton

added theorem Multiset.repeat_succ

added theorem Multiset.repeat_zero

added def Multiset.replicate

added theorem Multiset.singleton_add

added theorem Multiset.singleton_disjoint

added theorem Multiset.singleton_eq_cons_iff

added theorem Multiset.singleton_inj

added theorem Multiset.singleton_le

added theorem Multiset.singleton_ne_zero

added def Multiset.sizeOf

added theorem Multiset.sizeOf_lt_sizeOf_of_mem

added theorem Multiset.ssubset_cons

added def Multiset.strongDownwardInduction

added def Multiset.strongDownwardInductionOn

added theorem Multiset.strongDownwardInductionOn_eq

added theorem Multiset.strongDownwardInduction_eq

added def Multiset.strongInductionOn

added theorem Multiset.strongInductionOn_eq

added theorem Multiset.sub_add_inter

added theorem Multiset.sub_cons

added theorem Multiset.sub_eq_fold_erase

added theorem Multiset.sub_inter

added theorem Multiset.subset_cons

added theorem Multiset.subset_iff

added theorem Multiset.subset_of_le

added theorem Multiset.subset_zero

added def Multiset.subsingletonEquiv

added theorem Multiset.sup_eq_union

added theorem Multiset.toList_eq_nil

added theorem Multiset.toList_zero

added def Multiset.union

added theorem Multiset.union_add_distrib

added theorem Multiset.union_add_inter

added theorem Multiset.union_comm

added theorem Multiset.union_def

added theorem Multiset.union_le

added theorem Multiset.union_le_add

added theorem Multiset.union_le_iff

added theorem Multiset.union_le_union_left

added theorem Multiset.union_le_union_right

added theorem Multiset.wellFounded_lt

added theorem Multiset.zero_disjoint

added theorem Multiset.zero_inter

added theorem Multiset.zero_le

added theorem Multiset.zero_ne_cons

added theorem Multiset.zero_subset

added def Multiset.{u}

added def Multiset.«repeat»

deleted def Multiset

Created Mathlib/Init/Quot.lean