Theorem RelEmbedding.coe_mk

Modification history

2024-07-01 17:37

Mathlib/Order/RelIso/Basic.lean

chore(Order): remove almost all autoImplicit (#14304) …

Modified RelEmbedding.coe_mk View on Github →

2023-04-20 06:30

Mathlib/Order/RelIso/Basic.lean

chore: use FunLike.coe as coercion for OrderIso and RelEmbedding (#3082) …

Added RelEmbedding.coe_mk View on Github →