Possibly misleading `to_additive`

Stream: mathlib4

[Jihoon Hyun]

I was adding more instances to WithLp at #22434 . However simply adding instances brought an error, and it happened due to @[to_additive] at docs#MeasureTheory.continuous_integral_apply_neg_add . Also I found a suspicious naming, docs#instIsTopologicalAddGroupSum , which is also generated using @[to_additive] attached to docs#instIsTopologicalGroupProd . As I'm not familiar with to_additive, I'd like to get some advice or a possible fix, or a reason why I should not make a fix like #22434 .

[Eric Wieser]

Jihoon Hyun said:

Also I found a suspicious naming, docs#instIsTopologicalAddGroupSum , which is also generated using @[to_additive] attached to docs#instIsTopologicalGroupProd .

Manually setting the name to Prod.instIsTopologicalGroup should fix this, PR welcome

[Jihoon Hyun]

PR welcome

#22437

[Eric Wieser]

I pushed what might be a fix to #22434