mathlib

34a0c8c5 - chore(*): unify use of left and right for injectivity lemmas (#2655)

chore(*): unify use of left and right for injectivity lemmas (#2655) This is the evil twin of #2652 using the opposite convention: the name of a lemma stating that a function in two arguments is injective in one of the arguments refers to the argument that changes. Example: ```lean lemma sub_right_inj : a - b = a - c ↔ b = c ``` See also the [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/pow_(left.7Cright)_inj(ective)). This PR renames lemmas following the other convention. The following lemmas were renamed: `algebra/group/basic.lean`: * `mul_left_injective` ↔ `mul_right_injective` * `mul_left_inj` ↔ `mul_right_inj` * `sub_left_inj` ↔ `sub_right_inj` `algebra/goup/units.lean`: * `mul_left_inj` ↔ `mul_right_inj` * `divp_right_inj` → `divp_left_inj` `algebra/group_power.lean`: * `pow_right_inj` → `pow_left_inj` `algebra/group_with_zero.lean`: * `div_right_inj'` → ` div_left_inj'` * `mul_right_inj'` → `mul_left_inj'` `algebra/ring.lean`: * `domain.mul_right_inj` ↔ `domain.mul_left_inj` `data/finsupp.lean`: * `single_right_inj` → `single_left_inj` `data/list/basic.lean`: * `append_inj_left` ↔ `append_inj_right` * `append_inj_left'` ↔ `append_inj_right'` * `append_left_inj` ↔ `append_right_inj` * `prefix_append_left_inj` → `prefix_append_right_inj` `data/nat/basic.lean`: * `mul_left_inj` ↔ `mul_right_inj` `data/real/ennreal.lean`: * `add_left_inj` ↔ `add_right_inj` * `sub_left_inj` → `sub_right_inj` `set_theory/ordinal.lean`: * `mul_left_inj` → `mul_right_inj`