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: Dec 20 2023 at 11:08 UTC