Theorems · Theorem · order theory
Finset.range_eq_Ico
∀ (a : ℕ), Finset.range a = Finset.Ico 0 a
- Defined in
- Mathlib.Order.Interval.Finset.Nat
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Finset.rangestatement · cited by 1,341
- Finset.Icostatement · cited by 450
- Nat.Ico_zero_eq_rangeproof · cited by 25
Cited by26
Results whose statement or proof uses this declaration.
- sum_mul_eq_sub_sub_integral_mulproof · cited by 4
- eVariationOn.unionproof · cited by 4
- Nat.geom_sum_Ico_leproof · cited by 2
- Finset.sum_range_eq_add_Icoproof · cited by 2
- FormalMultilinearSeries.comp_partialSumproof · cited by 2
- harmonic_eq_sum_Iccproof · cited by 2
- Polynomial.sum_bernoulliproof · cited by 2
- HasFPowerSeriesWithinAt.compproof · cited by 2
- Finset.range_add_eq_unionproof · cited by 1
- Nat.sum_range_add_chooseproof · cited by 1
- Nat.sum_range_choose_halfwayproof · cited by 1
- Finset.sum_range_by_partsproof · cited by 1