Commit 2023-01-25 10:47 f47025ef

View on Github →

Feat: add a FunLike and an EmbeddingLike instance (#1488) Backported in leanprover-community/mathlib#18198.

Estimated changes

added theorem PEquiv.coe_mk
modified theorem PEquiv.ext
added theorem InitialSeg.ext
added theorem InitialSeg.map_rel_iff