mathlib documentation

data.multiset.range

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
@[simp]
@[simp]
theorem multiset.mem_range {m n : } :