Commit 2023-01-13 17:57 5456ba11

View on Github →

feat: port Data.Multiset.Fold (#1548)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Multiset/Fold.lean

added theorem Multiset.coe_fold_l

added theorem Multiset.coe_fold_r

added def Multiset.fold

added theorem Multiset.fold_add

added theorem Multiset.fold_bind

added theorem Multiset.fold_cons'_left

added theorem Multiset.fold_cons'_right

added theorem Multiset.fold_cons_left

added theorem Multiset.fold_cons_right

added theorem Multiset.fold_dedup_idem

added theorem Multiset.fold_distrib

added theorem Multiset.fold_eq_foldl

added theorem Multiset.fold_eq_foldr

added theorem Multiset.fold_hom

added theorem Multiset.fold_singleton

added theorem Multiset.fold_union_inter

added theorem Multiset.fold_zero

added theorem Multiset.le_smul_dedup

added theorem Multiset.max_le_of_forall_le

added theorem Multiset.max_nat_le_of_forall_le

Modified Mathlib/Init/Quot.lean