Topic: sum and prod notations
Kenny Lau (Jun 10 2020 at 02:36):
Why are the sum and prod notations localized in the locale
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