-
Notifications
You must be signed in to change notification settings - Fork 259
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] - feat: port Algebra.Ring.Ulift #1240
Conversation
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Mathlib/Algebra/Ring/Ulift.lean
Outdated
intCast_negSucc := AddGroupWithOne.intCast_negSucc } | ||
#align ulift.non_assoc_ring ULift.nonAssocRing | ||
|
||
-- Porting note: this doesn't work without `refine'` |
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.
I don't understand why this one is different. It also looks pretty slow.
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.
It's to do with the definitions of Int.cast
. The Int.cast
field for this instance is filled in automatically as the recursive definition, but it should be inherited from the Int.cast
instance on R
. This should be changed and same with Nat.cast
for this and the other instances.
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.
Adding natCast
and intCast
indeed fixed it, thanks!
bors merge |
Most of the porting consists of doing by hand what `pi_instance_derive_field` did. Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Most of the porting consists of doing by hand what
pi_instance_derive_field
did.