sum of function with domain fin d

Stream: new members

[Jelmer Firet]

Is there a function that does the following:

def sum {d : ℕ} (f : fin d → ℕ) : ℕ :=
f 0 + f 1 + ... + f (d-1)

if not, how do I define it?

[Mario Carneiro]

\sum i : fin n, f i

[Mario Carneiro]

import algebra.big_operators.basic
open_locale big_operators
def sum' {d : ℕ} (f : fin d → ℕ) : ℕ := ∑ i, f i

[Jelmer Firet]

That works, thanks