mathlib
e1ff2dff - chore(*): update `injective` lemma names to match the naming guide (#6740)

Commit
4 years ago
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`
Author
Parents
Loading