Theorems · Definition · combinatorics
Finset.range
ℕ → Finset ℕ
range n is the set of natural numbers less than n.
- Defined in
- Mathlib.Data.Finset.Range
- Cited by
- 1,341 results in Mathlib
- Foundations
- Depth 53 from the axioms, rests on 748 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Multiset.rangeproof · cited by 30
- Multiset.nodup_rangeproof · cited by 3
Cited by1,390
Results whose statement or proof uses this declaration.
- Finset.mem_rangestatement · cited by 140
- Finset.sum_range_succstatement and proof · cited by 121
- Nat.totientproof · cited by 111
- Finset.card_rangestatement · cited by 108
- eVariationOnproof · cited by 90
- Complex.exp_addproof · cited by 55
- wittPolynomialproof · cited by 54
- Complex.exp_zeroproof · cited by 43
- Nat.primesBelowproof · cited by 43
- Polynomial.bernoulliproof · cited by 41
- Finset.sum_range_succ'statement · cited by 37
- Finset.coe_rangestatement · cited by 33
Showing the 200 most cited of 1,390.