mathlib3

e8386bd4 - feat(group_theory/exponent): Define the exponent of a group (#10249)

feat(group_theory/exponent): Define the exponent of a group (#10249) This PR provides the definition and some very basic API for the exponent of a group/monoid. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>