mathlib

8430aae3 - feat(algebra/group_power/lemmas): More lemmas through `to_additive` (#13537)

feat(algebra/group_power/lemmas): More lemmas through `to_additive` (#13537) Use `to_additive` to generate a bunch of old `nsmul`/`zsmul` lemmas from new `pow`/`zpow` ones. Also protect `nat.nsmul_eq_mul` as it should have been.