Zulip Chat Archive
Stream: new members
Topic: set.sum?
Vaibhav Karve (Feb 25 2020 at 17:06):
Is there a set variant of list.sum?
Vaibhav Karve (Feb 25 2020 at 17:15):
list.sum is defined using list.foldl but there is no set variant of that either.
Scott Morrison (Feb 25 2020 at 17:22):
finset.sum, defined in algebra/big_operators.lean?
Scott Morrison (Feb 25 2020 at 17:23):
Remember a general set need not be finite!
Last updated: May 02 2025 at 03:31 UTC