Theorems · Theorem · group theory
Finset.sum_range_sub
∀ {G : Type u_3} [inst : AddCommGroup G] (f : ℕ → G) (n : ℕ), ∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0A telescoping sum along {0, ..., n - 1} of a function valued in a commutative
additive group reduces to the difference of the last and first terms.
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- Finset.sumstatement · cited by 5,195
- Finset.rangestatement · cited by 1,341
- sub_selfproof · cited by 996
- sub_add_sub_cancel'proof · cited by 18
- Finset.sum_range_inductionproof · cited by 4
Cited by15
Results whose statement or proof uses this declaration.
- MonotoneOn.eVariationOn_eqproof · cited by 4
- catalan_eq_centralBinom_divproof · cited by 3
- Monotone.cauchySeq_series_mul_of_tendsto_zero_of_boundedproof · cited by 2
- Finset.eq_sum_range_subproof · cited by 2
- AbsolutelyContinuousOnInterval.boundedVariationOnproof · cited by 2
- Complex.sin_mul_sum_cosproof · cited by 2
- Complex.sin_mul_sum_sinproof · cited by 2
- NormedAddCommGroup.completeSpace_of_summable_imp_tendstoproof · cited by 1
- Finset.sum_intervalGapsWithin_add_sum_eq_subproof · cited by 1
- MeasureTheory.mul_upcrossingsBefore_leproof · cited by 1
- MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm'proof · cited by 1
- MeasureTheory.stoppedValue_sub_eq_sumproof · cited by 1