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/algebra/restrict_scalars): replace restrict_scalars_smul_def
with version that does not commit defeq-abuse.
#18540
Conversation
…_def`. This lemma abuses definitional equality and I think we are better without it. My immediate motivation is the trouble it is causing in the Mathlib4 porting PR: leanprover-community/mathlib4#2563 Note that it was only used in one place and there is a better proof.
restrict_scalars_smul_def
.restrict_scalars_smul_def
.
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! Up to you whether you think the def
version is useful.
✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with |
restrict_scalars_smul_def
.restrict_scalars_smul_def
with version that does not commit defeq-abuse.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
bors merge |
👎 Rejected by label |
bors merge |
I'll fix the only remaining issue after leanprover-community/mathlib#18540 lands.
…ul_def` with version that does not commit defeq-abuse. (#18540) This lemma abuses definitional equality and I think we are better without it. My immediate motivation is the trouble it is causing in the Mathlib4 porting PR: leanprover-community/mathlib4#2563 Note that it was only used in one place and there is a better proof.
Pull request successfully merged into master. Build succeeded: |
restrict_scalars_smul_def
with version that does not commit defeq-abuse.restrict_scalars_smul_def
with version that does not commit defeq-abuse.
I did this manually --- is it possible to get mathport to do this?
This lemma abuses definitional equality and I think we are better without it. My immediate motivation is the trouble it is causing in the Mathlib4 porting PR: leanprover-community/mathlib4#2563
Note that it was only used in one place and there is a better proof.