Zulip Chat Archive

Stream: new members

Topic: sum of function with domain fin d


Jelmer Firet (Oct 31 2021 at 21:03):

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 (Oct 31 2021 at 21:12):

\sum i : fin n, f i

Mario Carneiro (Oct 31 2021 at 21:14):

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

Jelmer Firet (Oct 31 2021 at 21:16):

That works, thanks


Last updated: Dec 20 2023 at 11:08 UTC