Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

order of element #1563

Closed
jcommelin opened this issue Oct 17, 2019 · 1 comment
Closed

order of element #1563

jcommelin opened this issue Oct 17, 2019 · 1 comment
Labels
easy < 20s of review time. See the lifecycle page for guidelines. needs-refactor

Comments

@jcommelin
Copy link
Member

Currently the file group_theory/order_of_element is quite a mess: https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/order_of_element.lean

  • The first 10-15 declarations belong to other files
  • There is no additive version of the story. Need to add to_additive everywhere.
@jcommelin jcommelin added easy < 20s of review time. See the lifecycle page for guidelines. needs-refactor labels Oct 17, 2019
@eric-wieser
Copy link
Member

I've moved a single lemma in #5798

@eric-wieser eric-wieser mentioned this issue Jan 19, 2021
Closed
@Julian-Kuelshammer Julian-Kuelshammer mentioned this issue Mar 22, 2021
Closed
bors bot pushed a commit that referenced this issue Mar 31, 2021
@Julian-Kuelshammer
feat(group_theory/order_of_element): generalised to add_order_of (#6770)
cc5f2c4 
This PR defines `add_order_of` for an additive monoid. If someone sees how to do this with more automation, let me know. 

This gets one step towards closing issue #1563.

Coauthored by: Yakov Pechersky @pechersky 



Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
bors bot pushed a commit that referenced this issue Apr 1, 2021
@Julian-Kuelshammer
feat(group_theory/order_of_element): generalised to add_order_of (#6770)
d8de567 
This PR defines `add_order_of` for an additive monoid. If someone sees how to do this with more automation, let me know. 

This gets one step towards closing issue #1563.

Coauthored by: Yakov Pechersky @pechersky 



Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
b-mehta pushed a commit that referenced this issue Apr 2, 2021
@Julian-Kuelshammer @b-mehta
feat(group_theory/order_of_element): generalised to add_order_of (#6770)
c87625d 
This PR defines `add_order_of` for an additive monoid. If someone sees how to do this with more automation, let me know. 

This gets one step towards closing issue #1563.

Coauthored by: Yakov Pechersky @pechersky 



Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
@Julian-Kuelshammer Julian-Kuelshammer mentioned this issue Apr 4, 2021
Closed
@bors bors bot closed this as completed in 5312895 Apr 6, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
easy < 20s of review time. See the lifecycle page for guidelines. needs-refactor
Projects
None yet
Milestone
No milestone
2 participants
@eric-wieser @jcommelin