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

refactor(algebra/group/defs): Use nsmul in zsmul_rec #17826

Closed
wants to merge 3 commits into from
Closed

refactor(algebra/group/defs): Use nsmul in zsmul_rec #17826

wants to merge 3 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Dec 5, 2022 •
edited

Previously, zpow_rec/zsmul_rec would use npow_rec/nsmul_rec regardless on whether a better implementation was given.

Matches leanprover-community/mathlib4#862

Open in Gitpod

@YaelDillies YaelDillies mentioned this pull request Dec 5, 2022
Closed
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields etc) labels Dec 5, 2022
@eric-wieser
Copy link
Member

Do you have a case in mind where this comes up, and there is no better zpow/zsmul that should be built manually?

@eric-wieser eric-wieser 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 Dec 6, 2022
@YaelDillies
Copy link
Collaborator Author

Yes, and we talked about it a while ago: perm α has a nice pow coming from nat.iterate, but no nicer zpow than "case on the sign".

@eric-wieser eric-wieser removed the easy < 20s of review time. See the lifecycle page for guidelines. label Dec 9, 2022
@YaelDillies YaelDillies requested a review from a team as a code owner December 21, 2022 22:35
@YaelDillies YaelDillies mentioned this pull request Jan 7, 2023
Closed
@semorrison semorrison added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
@semorrison semorrison removed the request for review from a team August 6, 2023 09:55
@YaelDillies
Copy link
Collaborator Author

Now at leanprover-community/mathlib4#862

@YaelDillies YaelDillies deleted the zsmul_nsmul_rec branch March 23, 2024 15:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes t-algebra Algebra (groups, rings, fields etc) too-late This PR was ready too late for inclusion in mathlib3
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@YaelDillies @eric-wieser @semorrison