Commit 2021-08-16 03:52 b97344c0

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.