[Merged by Bors] - feat(GroupTheory/GroupAction): define MulAction.period and create GroupTheory/GroupAction/Period #9490

adri326 · 2024-01-06T14:42:50Z

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.

Note that the linter fails on Mathlib.Dynamic.PeriodicPts, since I do not know how to split the to_additive description on multiples lines :/

erdOne · 2024-01-06T15:12:18Z

Note that the linter fails on Mathlib.Dynamic.PeriodicPts, since I do not know how to split the to_additive description on multiples lines :/

I think a newline without indentation works, i.e.

@[to_additive "foo
bar"]
def

adri326 · 2024-01-06T15:32:02Z

Oh it does, thanks

erdOne

Some stylistic comments

Mathlib/Dynamics/PeriodicPts.lean

adri326 · 2024-01-07T11:37:59Z

Fixed the style issues pointed out above :)

Mathlib/Dynamics/PeriodicPts.lean

Vierkantor

Thanks for the PR. It might look like I have a lot of comments, but I'm confident that they'll be the (almost) complete set, once they're done everything is ready to merge. This PR is nicely structured overall!

Mathlib/Dynamics/PeriodicPts.lean

Mathlib/GroupTheory/GroupAction/Period.lean

Mathlib/Dynamics/PeriodicPts.lean

…ion.period with a few lemmas

…roofs

…dAction.period in header

…, small fixups

…dicPt_smul_iff

…eriod_smul instead

…period_one, period_inv, golfs First proving that `period m a | orderOf m` and `period m a | Monoid.exponent M` let me greatly golf the subsequent properties.

…ly docstring to `to_additive`

adri326 · 2024-02-14T20:07:53Z

Couple of changes, as suggested; of interest:

le_period_of_moved → le_period
moved_of_lt_period → pow_smul_ne_of_lt_period (currently lives in the MulAction namespace)
period_eq_one_of_fixed → period_eq_one_iff
new period_one and period_inv (I couldn't golf the latter any further)
new period_dvd_orderOf and period_dvd_exponent, which helped golfed the rest of the lemmas
added missing docstrings in @[to_additive]

Vierkantor

Some minor comments and I'm happy with this, thanks! I'm going to ask another maintainer to delegate this because I haven't reviewed Dynamics before and I contributed a few of the lemmas.

maintainer merge

Mathlib/Dynamics/PeriodicPts.lean

Mathlib/GroupTheory/GroupAction/Period.lean

github-actions · 2024-02-15T11:39:50Z

🚀 Pull request has been placed on the maintainer queue by Vierkantor.

github-actions · 2024-02-15T11:39:50Z

🚀 Pull request has been placed on the maintainer queue by Vierkantor.

…ve and move angle bracket Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

jcommelin

Thanks 🎉

bors merge

…upTheory/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.

mathlib-bors · 2024-02-15T14:03:51Z

Pull request successfully merged into master.

Build succeeded:

…upTheory/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.

adri326 added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) t-dynamics Dynamical Systems new-contributor This PR was made by a contributor with fewer than 5 merged PRs. Welcome to the community! labels Jan 6, 2024

erdOne reviewed Jan 6, 2024

View reviewed changes

adri326 mentioned this pull request Jan 7, 2024

chore: Replace Function.minimalPeriod (m • ·) a with MulAction.period m a #9514

Closed

2 tasks

tb65536 reviewed Jan 15, 2024

View reviewed changes

Mathlib/Dynamics/PeriodicPts.lean Show resolved Hide resolved

Vierkantor self-assigned this Feb 13, 2024

Vierkantor reviewed Feb 13, 2024

View reviewed changes

Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Feb 13, 2024

adri326 added 6 commits February 14, 2024 12:00

feat(GroupTheory/GroupAction): New Period module and implement MulAct…

c819dd2

…ion.period with a few lemmas

feat(Dynamic/PeriodicPts): define MulAction.period and prefer it in p…

8a606bf

…roofs

feat(Dynamic/PeriodicPts): add period_eq_one_of_fixed

80bfc1f

style(Dynamics/PeriodicPts): break line in to_additive and mention Ad…

af6f393

…dAction.period in header

style(Dynamics/PeriodicPts): minify proofs for MulAction.period

d880f9b

style(Dynamics/PeriodicPts): move and rename smul_pow_eq_function_pow…

e731985

…, small fixups

adri326 force-pushed the adri326/mulaction-period branch from 08af5bd to e731985 Compare February 14, 2024 11:31

adri326 added 5 commits February 14, 2024 12:35

style(Dynamics/PeriodicPts): rename fixed_iff_isPeriodicPt to isPerio…

63b4c79

…dicPt_smul_iff

style(Dynamics/PeriodicPts): prove pow_add_period_smul from pow_mod_p…

aff3c23

…eriod_smul instead

style(GroupTheory/GroupAction/Period): small golfs and style cleanups

41dff41

feat(GroupTheory/GroupAction/Period): lift period_eq_one_iff to iff, …

4dc1506

…period_one, period_inv, golfs First proving that `period m a | orderOf m` and `period m a | Monoid.exponent M` let me greatly golf the subsequent properties.

style(GroupTheory/GroupAction/Period): rename moved_of_lt_period, app…

feddce3

…ly docstring to `to_additive`

adri326 added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Feb 14, 2024

Vierkantor approved these changes Feb 15, 2024

View reviewed changes

Mathlib/Dynamics/PeriodicPts.lean Outdated Show resolved Hide resolved

Mathlib/GroupTheory/GroupAction/Period.lean Outdated Show resolved Hide resolved

adri326 and others added 2 commits February 15, 2024 12:47

style(GroupTheory/GroupAction/Period): missing docstring in to_additi…

989e487

…ve and move angle bracket Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

fix(Dynamics/PeriodicPts): fix line over 100 chars

90e1aa5

jcommelin approved these changes Feb 15, 2024

View reviewed changes

leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Feb 15, 2024

mathlib-bors bot changed the title ~~feat(GroupTheory/GroupAction): define MulAction.period and create GroupTheory/GroupAction/Period~~ [Merged by Bors] - feat(GroupTheory/GroupAction): define MulAction.period and create GroupTheory/GroupAction/Period Feb 15, 2024

mathlib-bors bot closed this Feb 15, 2024

mathlib-bors bot deleted the adri326/mulaction-period branch February 15, 2024 14:03

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(GroupTheory/GroupAction): define MulAction.period and create GroupTheory/GroupAction/Period #9490

[Merged by Bors] - feat(GroupTheory/GroupAction): define MulAction.period and create GroupTheory/GroupAction/Period #9490

adri326 commented Jan 6, 2024

erdOne commented Jan 6, 2024 •

edited

adri326 commented Jan 6, 2024

erdOne left a comment

adri326 commented Jan 7, 2024

Vierkantor left a comment

adri326 commented Feb 14, 2024

Vierkantor left a comment

github-actions bot commented Feb 15, 2024

github-actions bot commented Feb 15, 2024

jcommelin left a comment

mathlib-bors bot commented Feb 15, 2024

[Merged by Bors] - feat(GroupTheory/GroupAction): define MulAction.period and create GroupTheory/GroupAction/Period #9490

[Merged by Bors] - feat(GroupTheory/GroupAction): define MulAction.period and create GroupTheory/GroupAction/Period #9490

Conversation

adri326 commented Jan 6, 2024

erdOne commented Jan 6, 2024 • edited

adri326 commented Jan 6, 2024

erdOne left a comment

Choose a reason for hiding this comment

adri326 commented Jan 7, 2024

Vierkantor left a comment

Choose a reason for hiding this comment

adri326 commented Feb 14, 2024

Vierkantor left a comment

Choose a reason for hiding this comment

github-actions bot commented Feb 15, 2024

github-actions bot commented Feb 15, 2024

jcommelin left a comment

Choose a reason for hiding this comment

mathlib-bors bot commented Feb 15, 2024

erdOne commented Jan 6, 2024 •

edited