mathlib3

b31af6d9 - refactor(algebra/group): move `monoid.has_pow` etc to `algebra.group.defs` (#10147)

refactor(algebra/group): move `monoid.has_pow` etc to `algebra.group.defs` (#10147) This way we can state theorems about `pow`/`nsmul` using notation `^` and `•` right away. Also move some `ext` lemmas to a new file and rewrite proofs using properties of `monoid_hom`s. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>