Commit 2026-03-08 23:44 31672e22

feat: tag Pow.mk with to_additive (#36302) This PR uses the new reorder support in to_additive to automatically generate SMul instances from Pow instances. I've tried to address most such instances, but this is probably not exhaustive. I've also taken the opportunity to uniformize the instance names a bit. I wonder, should we change the order of the arguments in Monoid.npow : ℕ → M → M and npowRec to be consistent with the usual power operation, now that to_additive can support this kind of reordering? I suspect that the current ordering only exists for the sake of to_additive.