Multiset.range n
gives {0, 1, ..., n-1}
as a multiset. #
range n
is the multiset lifted from the list range n
,
that is, the set {0, 1, ..., n-1}
.
Equations
- Multiset.range n = ↑(List.range n)
Instances For
@[deprecated Multiset.notMem_range_self (since := "2025-05-23")]
Alias of Multiset.notMem_range_self
.