-
Notifications
You must be signed in to change notification settings - Fork 297
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] - refactor(algebra/module): rename smul_injective hx
to smul_left_injective M hx
#7577
Conversation
…jective M hx` This is a follow-up PR to #7548. * Now that there is also a `smul_right_injective`, we should disambiguate the previous `smul_injective` to `smul_left_injective`. * The `M` parameter can't be inferred from arguments before the colon, so we make it explicit.
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, thanks! Note we also have smul_left_cancel
which has different typeclass assumptions.
Good point. The assumptions are orthogonal enough though, that there is no easy way to unify them. |
bors d+ |
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
Whoops, forgot to commit the fix before pushing this branch and creating the PR :P |
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 r+
…jective M hx` (#7577) This is a follow-up PR to #7548. * Now that there is also a `smul_right_injective`, we should disambiguate the previous `smul_injective` to `smul_left_injective`. * The `M` parameter can't be inferred from arguments before the colon, so we make it explicit in `smul_left_injective` and `smul_right_injective`.
Pull request successfully merged into master. Build succeeded: |
smul_injective hx
to smul_left_injective M hx
smul_injective hx
to smul_left_injective M hx
This is a follow-up PR to #7548.
smul_right_injective
, we should disambiguate the previoussmul_injective
tosmul_left_injective
.M
parameter can't be inferred from arguments before the colon, so we make it explicit insmul_left_injective
andsmul_right_injective
.