-
Notifications
You must be signed in to change notification settings - Fork 316
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.
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
[Merged by Bors] - chore: get rid of erw
s in Mathlib.Algebra.Group.InjSurj
#17569
Conversation
Almost all of the `erw`s are actually just `rw`s. Only two places need additional rewriting: this is because the `pow_succ'` field of `DivInvMonoid`s mentions `Int.ofNat`, which is not reducibly defeq to the actual cast we use in our lemmas. This suggests we should redefine `pow_succ'` to use the actual cast instead.
PR summary 600253b2f0Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit> The doc-module for |
!bench |
Thanks 🎉 If CI passes, please remove the label bors d+ |
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
Here are the benchmark results for commit 600253b. |
Not sure why the linter is failing on the benchmark machine but the GitHub actions are passing. Are you happy to merge or do we want to debug this further first? |
Thanks 🎉 bors merge |
Almost all of the `erw`s work just fine as `rw`s. Only two places need additional rewriting: this is because the `pow_succ'` field of `DivInvMonoid`s mentions `Int.ofNat`, which is not reducibly defeq to the actual cast we use in our lemmas. This suggests we should redefine `pow_succ'` to use the actual cast instead: #17573.
Pull request successfully merged into master. Build succeeded: |
erw
s in Mathlib.Algebra.Group.InjSurjerw
s in Mathlib.Algebra.Group.InjSurj
Almost all of the
erw
s work just fine asrw
s. Only two places need additional rewriting: this is because thepow_succ'
field ofDivInvMonoid
s mentionsInt.ofNat
, which is not reducibly defeq to the actual cast we use in our lemmas.This suggests we should redefine
pow_succ'
to use the actual cast instead: #17573.