Theorems · Theorem · commutative algebra

Finset.sum_range_by_parts

∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : ℕ → R) (g : ℕ → M)
  (n : ℕ),
  ∑ i ∈ Finset.range n, f i • g i =
    f (n - 1) • ∑ i ∈ Finset.range n, g i -
      ∑ i ∈ Finset.range (n - 1), (f (i + 1) - f i) • ∑ i ∈ Finset.range (i + 1), g i

Summation by parts for ranges

Defined in

Mathlib.Algebra.BigOperators.Module

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule