Theorems · Theorem · group theory
Finset.sum_Ico_eq_sum_range
∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ → M) (m n : ℕ),
∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range (n - m), f (m + k)- Defined in
- Mathlib.Algebra.BigOperators.Intervals
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement and proof · cited by 5,195
- zero_addproof · cited by 2,366
- LT.lt.leproof · cited by 2,189
- Finset.rangestatement and proof · cited by 1,341
- Finset.Icostatement and proof · cited by 450
- not_leproof · cited by 328
- tsub_add_cancel_of_leproof · cited by 112
- Finset.sum_emptyproof · cited by 45
- tsub_eq_zero_iff_leproof · cited by 32
- Nat.Ico_zero_eq_rangeproof · cited by 25
Cited by10
Results whose statement or proof uses this declaration.
- dist_le_tsum_of_dist_le_of_tendstoproof · cited by 4
- Nat.Partition.hasProd_powerSeriesMk_card_countRestrictedproof · cited by 2
- AntitoneOn.summable_of_integrableOn_Ioiproof · cited by 2
- Polynomial.sum_bernoulliproof · cited by 2
- edist_le_tsum_of_edist_le_of_tendstoproof · cited by 2
- AntitoneOn.tsum_comp_add_le_integralproof · cited by 2
- HasFPowerSeriesWithinOnBall.tendsto_partialSum_prodproof · cited by 2
- AntitoneOn.integral_le_tsum_comp_addproof · cited by 1
- PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sqproof · cited by 1
- Complex.norm_exp_sub_sum_le_norm_mul_expproof · cited by 0