Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

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
Loading

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
@kim-em kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
@kim-em kim-em 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 subscribe to this conversation on GitHub. Already have an account? Sign in.
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.
3 participants
@YaelDillies @eric-wieser @kim-em