Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-27 10:18 3b590f31

View on Github →

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

Estimated changes

Modified src/logic/embedding.lean

modified def equiv.as_embedding

added theorem equiv.coe_eq_to_embedding

Created test/equiv.lean

added def f

added def s