Commit 2025-08-27 23:00 0c0fffb3

feat(to_additive): (dont_translate := ...) option (#28637) This PR adds the (dont_translate := ...) option to to_additive. This helps with additivizing delarations that have some multiplicative structure that can't be translated, such as a GroupWithZero, Ring or Field. Testing with this feature showed that firstMultiplicativeArg needed to be improved. That is also done by this PR (it is renamed to findMultiplicativeArg). In a future PR some automation may be added to infer these dont_translate arguments automatically based on the type of the declaration. For example if the type includes GroupWithZero G, then G will be automatically not translated. This PR now also uses this feature to use to_additive for as much as possible of MonoidAlgebra. #mathlib4 > to_additive on AddMonoidWithOne