Commit 2025-12-08 14:29 ed77abe8
View on Github →chore: additivise MulOpposite.op_finsuppSum to itself (#32501)
In to_additive there is this weird quirk about the implementation that when translating A.B, it looks for a translation of A.B and otherwise for a translation of just A, and tries that. This behavior causes trouble in #25273 and I must therefore tag MulOpposite.op_finsuppSum and a few other lemmas with to_additive self to make sure to_additive doesn't try to additivise them.