Zulip Chat Archive

Stream: new members

Topic: Using big operators


view this post on Zulip Bolton Bailey (Jan 29 2021 at 07:04):

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

view this post on Zulip Bryan Gin-ge Chen (Jan 29 2021 at 07:07):

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

view this post on Zulip Bolton Bailey (Jan 29 2021 at 07:11):

Yep that does it, thanks


Last updated: May 13 2021 at 18:26 UTC