Commit 2020-05-12 15:37 34a0c8c5

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:

lemma sub_right_inj : a - b = a - c ↔ b = c

See also the Zulip discussion. 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