Commit 2021-03-18 19:27 e1ff2dff

chore(*): update injective lemma names to match the naming guide (#6740) In src/algebra/group_ring_action.lean:

• injective_to_semiring_hom -> to_semiring_hom_injective In src/algebra/module/linear_map.lean:
• linear_equiv.injective_to_equiv -> linear_equiv.to_equiv_injective
• linear_equiv.injective_to_linear_map -> linear_equiv.to_linear_map_injective In src/analysis/normed_space/enorm.lean:
• enorm.injective_coe_fn -> enorm.coe_fn_injective In src/data/equiv/basic.lean:
• equiv.injective_coe_fn -> equiv.coe_fn_injective In src/data/real/nnreal.lean:
• nnreal.injective_coe -> nnreal.coe_injective In src/data/sum.lean:
• sum.injective_inl -> sum.inl_injective
• sum.injective_inr -> sum.inr_injective In src/linear_algebra/affine_space/affine_equiv.lean:
• affine_equiv.injective_to_affine_map -> affine_equiv.to_affine_map_injective
• affine_equiv.injective_coe_fn -> affine_equiv.coe_fn_injective
• affine_equiv.injective_to_equiv -> affine_equiv.to_equiv_injective In src/linear_algebra/affine_space/affine_map.lean:
• affine_map.injective_coe_fn -> affine_map.coe_fn_injective In src/measure_theory/outer_measure.lean:
• measure_theory.outer_measure.injective_coe_fn -> measure_theory.outer_measure.coe_fn_injective In src/order/rel_iso.lean:
• rel_iso.injective_to_equiv -> rel_iso.to_equiv_injective
• rel_iso.injective_coe_fn -> rel_iso.coe_fn_injective In src/topology/algebra/module.lean:
• continuous_linear_map.injective_coe_fn -> continuous_linear_map.coe_fn_injective