## Stream: general

### Topic: sum and prod notations

#### Kenny Lau (Jun 10 2020 at 02:36):

Why are the sum and prod notations localized in the locale big_operators?

#### Johan Commelin (Jun 10 2020 at 06:31):

@Kenny Lau Because we might want to reuse the notation in another context...

#### Johan Commelin (Jun 10 2020 at 06:32):

If we all agree that this will not happen... then we can make it global notation.

Last updated: May 13 2021 at 18:26 UTC