Commit 2023-01-13 18:51 e609eeb4

View on Github →

feat: port Data.Multiset.FinsetOps (#1547)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Multiset/Basic.lean

added theorem Multiset.union_zero

added theorem Multiset.zero_union

Created Mathlib/Data/Multiset/FinsetOps.lean

added theorem Multiset.Nodup.ndinsert

added theorem Multiset.Nodup.ndinter

added theorem Multiset.Nodup.ndunion

added theorem Multiset.attach_ndinsert

added theorem Multiset.coe_ndinsert

added theorem Multiset.coe_ndinter

added theorem Multiset.coe_ndunion

added theorem Multiset.cons_ndinter_of_mem

added theorem Multiset.cons_ndunion

added theorem Multiset.dedup_add

added theorem Multiset.dedup_cons

added theorem Multiset.disjoint_ndinsert_left

added theorem Multiset.disjoint_ndinsert_right

added theorem Multiset.inter_le_ndinter

added theorem Multiset.le_ndinsert_self

added theorem Multiset.le_ndinter

added theorem Multiset.le_ndunion_left

added theorem Multiset.le_ndunion_right

added theorem Multiset.length_ndinsert_of_mem

added theorem Multiset.length_ndinsert_of_not_mem

added theorem Multiset.mem_ndinsert

added theorem Multiset.mem_ndinsert_of_mem

added theorem Multiset.mem_ndinsert_self

added theorem Multiset.mem_ndinter

added theorem Multiset.mem_ndunion

added def Multiset.ndinsert

added theorem Multiset.ndinsert_le

added theorem Multiset.ndinsert_of_mem

added theorem Multiset.ndinsert_of_not_mem

added theorem Multiset.ndinsert_zero

added def Multiset.ndinter

added theorem Multiset.ndinter_cons_of_not_mem

added theorem Multiset.ndinter_eq_inter

added theorem Multiset.ndinter_eq_zero_iff_disjoint

added theorem Multiset.ndinter_le_left

added theorem Multiset.ndinter_le_right

added theorem Multiset.ndinter_subset_left

added theorem Multiset.ndinter_subset_right

added def Multiset.ndunion

added theorem Multiset.ndunion_eq_union

added theorem Multiset.ndunion_le

added theorem Multiset.ndunion_le_add

added theorem Multiset.ndunion_le_union

added theorem Multiset.subset_ndunion_left

added theorem Multiset.subset_ndunion_right

added theorem Multiset.zero_ndinter

added theorem Multiset.zero_ndunion