Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-18 22:26 ed44541a

View on Github →

chore(*): regularize naming using injective (#3071) This begins some of the naming regularization discussed at Some general rules:

  1. Lemmas should have injective in the name iff they have injective in the conclusion
  2. X_injective is preferable to injective_X.
  3. Unidirectional inj lemmas should be dropped in favour of bidirectional ones. Mostly, this PR tried to fix the names of lemmas that conclude injective (also surjective and bijective, but they seemed to be much better already). A lot of the changes are from injective_X to X_injective style

Estimated changes

deleted theorem of_add_inj
added theorem of_add_injective
deleted theorem of_mul_inj
added theorem of_mul_injective
deleted theorem to_add_inj
added theorem to_add_injective
deleted theorem to_mul_inj
added theorem to_mul_injective
modified theorem submodule.coe_set_eq
deleted theorem submodule.ext'
modified theorem submodule.ext
added theorem fin.cast_le_injective
deleted theorem fin.injective_cast_le
deleted theorem fin.injective_cast_succ
deleted theorem fin.injective_succ
deleted theorem fin.injective_val
added theorem fin.succ_injective
added theorem fin.val_injective
deleted theorem list.cons_inj'
modified theorem list.cons_inj
added theorem list.cons_injective
deleted theorem list.injective_length
deleted theorem list.injective_length_iff
deleted theorem list.injective_map_iff
added theorem list.length_injective
added theorem list.map_injective_iff
deleted theorem list.mem_map_of_inj
deleted theorem dim_eq_injective
added theorem dim_eq_of_injective
added theorem dim_eq_of_surjective
deleted theorem dim_eq_surjective
deleted theorem dim_le_injective
added theorem dim_le_of_injective
added theorem dim_le_of_surjective
deleted theorem dim_le_surjective