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(data/equiv/basic): lemmas about composition with equivalences #10693
Conversation
antoinelab01
commented
Dec 9, 2021
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
I think I fixed all the errors, but for some reason the linter is still unhappy |
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 seems odd to me that linear_equiv.eq_comp_symm
is about linear_map.comp
, but mul_equiv.eq_comp_symm
is not about monoid_hom.comp
(and instead is about function.comp
like equiv.eq_comp_symm
).
I think we should probably rename the lemmas about linear_map.comp
from eq_comp_symm
to eq_comp_to_linear_map_symm
, which frees up the existing names to hold the lemmas about function.comp
.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Done! |
Thanks! Can you add the |
Done! |
@eric-wieser This PR got kind of forgotten, any chance it could be merged soon? (or let me know if it still needs changes) |
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+
Just a small style comment to address
✌️ antoinelab01 can now approve this pull request. To approve and merge a pull request, simply reply with |
Since this has sat around for a while, can you make sure to merge master and wait for CI before merging? |
bors r+ |
…10693) Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Build failed (retrying...): |
…10693) Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |