Commit 2022-11-24 08:51 6bf4de4d

fix(Algebra/Group/Defs): make to_additive play nice with pow and smul (#706) The additivization of pow was borked because Pow.pow is really HPow.hPow under the hood via the instance instHPow. Consequently, it was useful to create a heterogeneous SMul type class HSMul, through which the • notation now derives. The upshot is that to_additive can now handle lemmas involving pow as is seen in a few places in this PR, thereby fixing some TODOs. Note that this also makes it possible to port files rapidly approaching (e.g., Algebra/Group/InjSurj.lean) without resorting to nasty hacks or omitting the additive versions. See the discussion on Zulip