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