mathlib documentation

data.​multiset.​range

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]

@[simp]
theorem multiset.​mem_range {m n : } :