Commit 2023-01-13 17:39 2b906934

View on Github →

feat: port Data.Multiset.Sum (#1546)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Multiset/Sum.lean

added theorem Multiset.card_disjSum

added def Multiset.disjSum

added theorem Multiset.disjSum_lt_disjSum_of_le_of_lt

added theorem Multiset.disjSum_lt_disjSum_of_lt_of_le

added theorem Multiset.disjSum_mono

added theorem Multiset.disjSum_mono_left

added theorem Multiset.disjSum_mono_right

added theorem Multiset.disjSum_strictMono_left

added theorem Multiset.disjSum_strictMono_right

added theorem Multiset.disjSum_zero

added theorem Multiset.inl_mem_disjSum

added theorem Multiset.inr_mem_disjSum

added theorem Multiset.mem_disjSum

added theorem Multiset.zero_disjSum