Theorems · Definition · combinatorics
Multiset.range
ℕ → Multiset ℕ
range n is the multiset lifted from the list range n,
that is, the set {0, 1, ..., n-1}.
- Defined in
- Mathlib.Data.Multiset.Range
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement · cited by 2,627
- Multiset.ofListproof · cited by 290
Cited by31
Results whose statement or proof uses this declaration.
- Finset.rangeproof · cited by 1,341
- Multiset.map_toEnumFinset_fstproof · cited by 7
- Multiset.card_rangestatement · cited by 5
- Finset.range_valstatement · cited by 4
- Polynomial.iterate_derivative_mulproof · cited by 4
- Nat.Subtype.exists_succproof · cited by 3
- Multiset.map_fst_le_of_subset_toEnumFinsetproof · cited by 3
- Multiset.prod_X_add_C_eq_sum_esymmproof · cited by 3
- Multiset.nodup_rangestatement · cited by 3
- IsPrimitiveRoot.nthRoots_eqstatement and proof · cited by 3
- IsPrimitiveRoot.card_nthRootsproof · cited by 2
- Multiset.bind_powerset_lenstatement and proof · cited by 2