Using big operators

Stream: new members

[Bolton Bailey]

Not sure why the second one below gives the error "unexpected token". What am I doing wrong?

import algebra.big_operators.basic

section

parameters {m : ℕ}

parameters {b : fin m → ℕ}

def foo  : ℕ :=
  finset.sum (finset.fin_range m) (λ i, (b i) )


def bar  : ℕ :=
  ∑ i in (finset.fin_range m), b

end

[Bryan Gin-ge Chen]

To use the ∑ i in ... notation you should add open_locale big_operators somewhere above that definition. (You're also missing an i at the end):

import algebra.big_operators.basic

section

parameters {m : ℕ}

parameters {b : fin m → ℕ}

def foo  : ℕ :=
  finset.sum (finset.fin_range m) (λ i, (b i) )

open_locale big_operators
def bar  : ℕ :=
  ∑ i in (finset.fin_range m), b i

end

[Bolton Bailey]

Yep that does it, thanks