Commit 2020-10-20 10:23 cf551ee3

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.