Theorem PEquiv.ext

Modification history

2023-01-25 10:47

Mathlib/Data/PEquiv.lean

Feat: add a `FunLike` and an `EmbeddingLike` instance (#1488) …

Modified PEquiv.ext View on Github →

2022-12-14 13:31

Mathlib/Data/PEquiv.lean

feat port: Data.PEquiv (#1008) …

Added PEquiv.ext View on Github →