Zulip Chat Archive

Stream: general

Topic: Documentation bugs in multiset


Robert Maxton (Jun 07 2022 at 12:28):

Before I forget -- it seems some of the source links in multiset go to the wrong places. Forexample, docs#multiset.sum_add links to https://github.com/leanprover-community/mathlib/blob/de648fd51be82c29292e25a5912fd492683ef876/src/algebra/big_operators/multiset.lean#L70, which is prod_add; docs#multiset.prod_add

Robert Maxton (Jun 07 2022 at 12:28):

... in fact the problem appears to be mostly with sum_<foo> in general

Reid Barton (Jun 07 2022 at 12:31):

https://leanprover-community.github.io/mathlib_docs/attributes.html#to_additive

Reid Barton (Jun 07 2022 at 12:47):

There's no separate source for sum_add, it is generated automatically from prod_add.


Last updated: Dec 20 2023 at 11:08 UTC