Commit 2020-06-18 22:26 ed44541a

chore(*): regularize naming using injective (#3071) This begins some of the naming regularization discussed at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/naming.20of.20injectivity.20lemmas 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