Commit 2021-05-12 10:02 6b62b9f7

refactor(algebra/module): rename smul_injective hx to smul_left_injective 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.