mathlib
eb46e7e3 - feat(algebra/group/to_additive): let to_additive turn `pow` into `nsmul` (#12477)

Commit
3 years ago
feat(algebra/group/to_additive): let to_additive turn `pow` into `nsmul` (#12477) The naming convention for `npow` in lemma names is `pow`, so let’s teach `to_additive` about it. A fair number of lemmas now no longer need an explicit additive name.
Author
Parents
Loading