mathlib

e6f4852b - feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g (#10767)

feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g (#10767) Precursor to #10692. Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>