Commit 2023-01-13 11:21 090a8a08

View on Github →

feat: port Data.Multiset.Range (#1528)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Multiset/Range.lean

added theorem Multiset.card_range

added theorem Multiset.coe_range

added theorem Multiset.mem_range

added theorem Multiset.not_mem_range_self

added def Multiset.range

added theorem Multiset.range_add

added theorem Multiset.range_add_eq_union

added theorem Multiset.range_disjoint_map_add

added theorem Multiset.range_subset

added theorem Multiset.range_succ

added theorem Multiset.range_zero

added theorem Multiset.self_mem_range_succ