Documentation

Mathlib.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
Instances For
    @[simp]
    theorem Multiset.card_range (n : ) :
    Multiset.card (Multiset.range n) = n
    @[simp]
    theorem Multiset.mem_range {m : } {n : } :
    theorem Multiset.range_add (a : ) (b : ) :