Zulip Chat Archive
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 02 2025 at 03:31 UTC