bigops notation

Stream: general

[Johan Commelin]

It seems that the docs aren't using localized notation:
https://leanprover-community.github.io/mathlib_docs/algebra/big_operators.html
doesn't use \prod or \sum.