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

Commit

4 years ago

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.

Author

apurvnakade

Parents

68aada0d

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

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