Theorem PEquiv.coe_mk

Modification history

2023-01-25 10:47
Mathlib/Data/PEquiv.lean
Feat: add a `FunLike` and an `EmbeddingLike` instance (#1488) …
Added PEquiv.coe_mkView on Github →