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(*): Fix mistakes #18654
Conversation
class non_assoc_ring (α : Type*) extends | ||
non_unital_non_assoc_ring α, non_assoc_semiring α, add_group_with_one α | ||
non_unital_non_assoc_ring α, non_assoc_semiring α, add_comm_group_with_one α |
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.
Can you make a forward-port of just this line and check it doesn't cause any TC problems in CI? The rest of the forward-port can be committed later.
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 just checked and NonAssocRing
already extends AddCommGroupWithOne
.
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+
Looks good, but please check that mathlib4 CI is happy with the change to the extends
clause before merging here.
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Fix naming errors and non-defeq diamonds recently introduced. Those were discovered during the port.
Pull request successfully merged into master. Build succeeded: |
Match leanprover-community/mathlib#18654 * [`algebra.group.opposite`@`acebd8d49928f6ed8920e502a6c90674e75bd441`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/opposite?range=acebd8d49928f6ed8920e502a6c90674e75bd441..76de8ae01554c3b37d66544866659ff174e66e1f) * [`algebra.ring.defs`@`314d3a578607dbd2eb2481ab15fceeb62b36cbdb`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/defs?range=314d3a578607dbd2eb2481ab15fceeb62b36cbdb..76de8ae01554c3b37d66544866659ff174e66e1f) * [`algebra.ring.opposite`@`acebd8d49928f6ed8920e502a6c90674e75bd441`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/opposite?range=acebd8d49928f6ed8920e502a6c90674e75bd441..76de8ae01554c3b37d66544866659ff174e66e1f) * [`algebra.field.opposite`@`acebd8d49928f6ed8920e502a6c90674e75bd441`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/field/opposite?range=acebd8d49928f6ed8920e502a6c90674e75bd441..76de8ae01554c3b37d66544866659ff174e66e1f)
Match leanprover-community/mathlib#18654 * [`algebra.group.opposite`@`acebd8d49928f6ed8920e502a6c90674e75bd441`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/opposite?range=acebd8d49928f6ed8920e502a6c90674e75bd441..76de8ae01554c3b37d66544866659ff174e66e1f) * [`algebra.ring.defs`@`314d3a578607dbd2eb2481ab15fceeb62b36cbdb`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/defs?range=314d3a578607dbd2eb2481ab15fceeb62b36cbdb..76de8ae01554c3b37d66544866659ff174e66e1f) * [`algebra.ring.opposite`@`acebd8d49928f6ed8920e502a6c90674e75bd441`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/opposite?range=acebd8d49928f6ed8920e502a6c90674e75bd441..76de8ae01554c3b37d66544866659ff174e66e1f) * [`algebra.field.opposite`@`acebd8d49928f6ed8920e502a6c90674e75bd441`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/field/opposite?range=acebd8d49928f6ed8920e502a6c90674e75bd441..76de8ae01554c3b37d66544866659ff174e66e1f)
Match leanprover-community/mathlib#18654 * [`algebra.group.opposite`@`acebd8d49928f6ed8920e502a6c90674e75bd441`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/opposite?range=acebd8d49928f6ed8920e502a6c90674e75bd441..76de8ae01554c3b37d66544866659ff174e66e1f) * [`algebra.ring.defs`@`314d3a578607dbd2eb2481ab15fceeb62b36cbdb`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/defs?range=314d3a578607dbd2eb2481ab15fceeb62b36cbdb..76de8ae01554c3b37d66544866659ff174e66e1f) * [`algebra.ring.opposite`@`acebd8d49928f6ed8920e502a6c90674e75bd441`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/ring/opposite?range=acebd8d49928f6ed8920e502a6c90674e75bd441..76de8ae01554c3b37d66544866659ff174e66e1f) * [`algebra.field.opposite`@`acebd8d49928f6ed8920e502a6c90674e75bd441`..`76de8ae01554c3b37d66544866659ff174e66e1f`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/field/opposite?range=acebd8d49928f6ed8920e502a6c90674e75bd441..76de8ae01554c3b37d66544866659ff174e66e1f)
Fix naming errors and non-defeq diamonds recently introduced. Those were discovered during the port.