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(algebra/ring/ulift): Split off and golf field instances #18590
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
👎 Rejected by label |
Just fixed the lint so it will go through. bors merge |
Move field-like instances on `ulift` from `algebra.ring.ulift` to a new file `algebra.field.ulift`. Golf them by declaring the `has_nat_cast` and `has_int_cast` instances earlier.
Pull request successfully merged into master. Build succeeded: |
Match leanprover-community/mathlib#18590 and leanprover-community/mathlib#18596 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Match leanprover-community/mathlib#18590 and leanprover-community/mathlib#18596 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Move field-like instances on
ulift
fromalgebra.ring.ulift
to a new filealgebra.field.ulift
. Golf them by declaring thehas_nat_cast
andhas_int_cast
instances earlier.Match leanprover-community/mathlib4#2911