mathlib documentation

data.multiset.range

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 : } :