feat(algebra/module): scalar multiplication on the right is injective #7548
Conversation
Vierkantor
added
the
awaiting-review
This is a split-off dependency from #7496
| @@ -461,9 +461,17 @@ end add_comm_group | |||
|
|
|||
| section module | |||
|
|
|||
| variables {R} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] | |||
|
|
|||
| lemma smul_right_injective {x : M} (hx : x ≠ 0) : | |||
There was a problem hiding this comment.
I think R should probably be explicit here. Is M explicit for smul_left_injective?
There was a problem hiding this comment.
Both R and M are implicit in smul_left_injective. I guess it depends whether we want to treat injective like iff, that arguments inferable from applying injective can be left implicit.
I could also wait for #7496 to be merged, then open a PR for making the parameters for smul_left_injective and for smul_right_injective explicit.
There was a problem hiding this comment.
I must have been imagining that smul_left_injective even exists; I found mul_action.injective, but that's implicit anyway.
PatrickMassot
added
awaiting-author
Vierkantor
added
awaiting-review
There was a problem hiding this comment.
bors d+
I don't know how you want to handle this and #7496, perhaps there's no need to put this one on the queue.
| @@ -461,9 +461,17 @@ end add_comm_group | |||
|
|
|||
| section module | |||
|
|
|||
| variables {R} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] | |||
|
|
|||
| lemma smul_right_injective {x : M} (hx : x ≠ 0) : | |||
There was a problem hiding this comment.
I must have been imagining that smul_left_injective even exists; I found mul_action.injective, but that's implicit anyway.
|
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
I expect that will be the case, but I'll keep an eye on it. |
|
Everything has been merged already, so closing this PR. |
Vierkantor
removed
the
delegated
…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.
…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`.
This is a split-off dependency from #7496.