Yaël Dillies (Mar 10 2022 at 21:23):
docs#finset.sum_comp is weirdly declared. Instead of tagging docs#finset.prod_comp, it was additivized by hand and later tagged
to_additive. The later tagging adds a docstring, as shown by the source, but it seems to get ignored because it's not visible in the docs.
Last updated: Aug 03 2023 at 10:10 UTC