feat(group_theory/submonoid/membership): upgrade definition of pow from a set morphism to a monoid morphism (#10898)
feat(group_theory/submonoid/membership): upgrade definition of pow from a set morphism to a monoid morphism (#10898)

This comes at no extra cost. All the prerequisite definitions and lemmas were already in mathlib.





leanprover-community/mathlib,leanprover-community/mathlib