mathlib3

cf551ee3 - chore(*): review some lemmas about injectivity of coercions (#4711)

chore(*): review some lemmas about injectivity of coercions (#4711) API changes: * rename `linear_map.coe_fn_congr` to `protected linear_map.congr_arg`; * rename `linear_map.lcongr_fun` to `protected linear_map.congr_fun`; * rename `enorm.coe_fn_injective` to `enorm.injective_coe_fn`, add `enorm.coe_inj`; * rename `equiv.coe_fn_injective` to `equiv.injective_coe_fn`, reformulate in terms of `function.injective`; * add `equiv.coe_inj`; * add `affine_map.injective_coe_fn`, `protected affine_map.congr_arg`, and `protected affine_map.congr_fun`; * rename `linear_equiv.to_equiv_injective` to `linear_equiv.injective_to_equiv`, add `linear_equiv.to_equiv_inj`; * rename `linear_equiv.eq_of_linear_map_eq` to `linear_equiv.injective_to_linear_map`, formulate as `injective coe`; * add `linear_equiv.to_linear_map_inj`; * rename `outer_measure.coe_fn_injective` to `outer_measure.injective_coe_fn`; * rename `rel_iso.to_equiv_injective` to `rel_iso.injective_to_equiv`; * rename `rel_iso.coe_fn_injective` to `rel_iso.injective_coe_fn`; * rename `continuous_linear_map.coe_fn_injective` to `injective_coe_fn`.