Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.coe_eq_to_embedding

Modification history

2021-07-27 10:18

src/logic/embedding.lean

feat(logic/embedding): add a coe instance from equiv to embeddings (#8323)

Added equiv.coe_eq_to_embedding View on Github →