Theorems · Theorem · group theory

Finset.sum_range_induction

∀ {M : Type u_4} [inst : AddCommMonoid M] (f s : ℕ → M),
  s 0 = 0 → ∀ (n : ℕ), (∀ k < n, s (k + 1) = s k + f k) → ∑ k ∈ Finset.range n, f k = s n

For any sum along {0, ..., n - 1} of a commutative-monoid-valued function, we can verify that it's equal to a different function just by checking differences of adjacent terms up to n. This is a discrete analogue of the fundamental theorem of calculus.

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Basic

Cited by

4 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoid