Theorems · Definition · combinatorics

Fin.partialSum

{M : Type u_2} → [AddMonoid M] → {n : ℕ} → (Fin n → M) → Fin (n + 1) → M

For f = (a₁, ..., aₙ) in αⁿ, partialSum f is (0, a₁, a₁ + a₂, ..., a₁ + ... + aₙ) in αⁿ⁺¹.

Defined in

Mathlib.Algebra.BigOperators.Fin

Cited by

10 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms

Assumes

AddMonoid