Commit 2024-02-15 13:05 30a9315c

feat(GroupTheory/GroupAction): define MulAction.period and create GroupTheory/GroupAction/Period (#9490) Defines MulAction.period g a as a wrapper around Function.minimalPeriod (fun x => g • x) a, allowing for some cleaner proofs involving the period of a group action. The existing MulAction.*_minimalPeriod_* lemmas are changed to be defined using their now-preferred MulAction.*_period_* counterparts, although they will only be made deprecated in another pull request. The Mathlib.GroupTheory.GroupAction.Period module is also created, for additional lemmas around MulAction.period. Some core lemmas need to remain in Mathlib.Dynamics.PeriodicPts, as they are needed for ZMod and the quotient group.