Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.embedding.coe_injective

Modification history

2022-01-25 10:49
src/logic/embedding.lean
feat(data/fun_like): define `embedding_like` and `equiv_like` (#10759) …
Modified function.embedding.coe_injectiveView on Github →
2021-04-28 01:28
src/logic/embedding.lean
feat(logic/embedding): add function.embedding.coe_injective (#7383) …
Added function.embedding.coe_injectiveView on Github →