Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.as_embedding

Modification history

2021-07-27 10:18
src/logic/embedding.lean
feat(logic/embedding): add a coe instance from equiv to embeddings (#8323)
Modified equiv.as_embeddingView on Github →
2021-04-07 06:34
src/logic/embedding.lean
feat(data/*set): some finite sets lemmas (#7037)
Added equiv.as_embeddingView on Github →