Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.coe_fn_injective

Modification history

2022-10-18 21:51
src/logic/equiv/basic.lean
chore(logic/equiv/basic): split into two files (#17038) …
Modified equiv.coe_fn_injectiveView on Github →
2022-01-25 10:49
src/data/equiv/basic.lean
feat(data/fun_like): define `embedding_like` and `equiv_like` (#10759) …
Modified equiv.coe_fn_injectiveView on Github →
2021-07-22 14:12
src/data/equiv/basic.lean
chore(*): Prevent lemmas about the injectivity of `coe_fn` introducing un-reduced lambda terms (#8386) …
Modified equiv.coe_fn_injectiveView on Github →
2021-03-18 19:27
src/data/equiv/basic.lean
chore(*): update `injective` lemma names to match the naming guide (#6740) …
Added equiv.coe_fn_injectiveView on Github →
2020-10-20 10:23
src/data/equiv/basic.lean
chore(*): review some lemmas about injectivity of coercions (#4711) …
Deleted equiv.coe_fn_injectiveView on Github →
2020-05-23 07:44
src/data/equiv/basic.lean
chore(data/equiv): make `equiv.ext` args use { } (#2776) …
Added equiv.coe_fn_injectiveView on Github →