Finite partial sums

This file contains basic facts about finite partial sums.

Main results

• TauCeti.eq_zero_of_forall_sum_Iic_eq_zero: a finite sequence whose inclusive partial sums all vanish is zero.

theorem TauCeti.eq_zero_of_forall_sum_Iic_eq_zero {M : Type u_1} [AddCommMonoid M] (n : ℕ) {y : Fin (n + 1) → M} (hy : ∀ (k : Fin (n + 1)), ∑ j ≤ k, y j = 0) : y = 0

A finite sequence all of whose inclusive partial sums vanish is zero.