mathlib

b97344c0 - chore(algebra/module): Swap the naming of `smul_(left|right)_injective` to match the naming guide (#8659)

chore(algebra/module): Swap the naming of `smul_(left|right)_injective` to match the naming guide (#8659) The naming conventions say: > An injectivity lemma that uses "left" or "right" should refer to the argument that "changes". For example, a lemma with the statement `a - b = a - c ↔ b = c` could be called `sub_right_inj`. This corrects the name of `function.injective (λ c : R, c • x)` to be `smul_left_injective` instead of the previous `smul_right_injective`, and vice versa for `function.injective (λ x : M, r • x)`. This also brings it in line with `mul_left_injective` and `mul_right_injective`.