basic): add `smul_right_inj` (#12252)

Commit

3 years ago

feat(algebra/module/basic): add `smul_right_inj` (#12252) Also golf the proof of `smul_right_injective` by reusing `add_monoid_hom.injective_iff`.

Author

urkud

Parents