Commit 2021-12-23 22:35 1db0052e
View on Github →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.