Commit 2025-12-05 12:39 ce740694

chore(Algebra/MonoidAlgebra): use to_additive more (#32398) Using Jovan's new dont_translate syntax, we can tag much more of the MonoidAlgebra API with to_additive. A few points:

1. to_additive currently doesn't support the destructing have syntax, because it generates an auxiliary match statement. The corresponding obtain syntax is fine though.
2. AddMonoidAlgebra.opRingEquiv and MonoidAlgebra.opRingEquiv were not the same statement (up to additivisation): The first assumed commutativity of the base monoid to get rid of an AddOpposite in the RHS. Using to_additive makes the type signatures align, at the cost of some shuffling around in later files. This shuffling around will become trivial after #32254.