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: remove redundant LinearEquiv.map_neg/sub #12330
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.
Looks good to me.
#align linear_equiv.map_neg map_negₓ | ||
#align linear_equiv.map_sub map_subₓ |
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.
What's the significance of the little x
here?
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.
The porting wiki contains this:
"when mathport suggests that you add ₓ in the name of an #align statement, figure out why it wants that and leave a porting note. Common reasons are:
- a change in the order of universe variables, typeclass arguments or implicit arguments
- some other defeq change, due to a change deep down in core or std."
See also https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#aligning-names.
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 means that the types don't match up exactly; in this case the new lemma is much more general.
I think this is useful to keep as sometimes |
I have not experienced that |
Thanks! bors merge |
These are redundant with `_root_.{map_neg,map_sub}`.
Pull request successfully merged into master. Build succeeded: |
These are redundant with `_root_.{map_neg,map_sub}`.
These are redundant with `_root_.{map_neg,map_sub}`.
These are redundant with
_root_.{map_neg,map_sub}
.