Def OrderIsoClass.toOrderIso

Modification history

2024-02-05 18:00

Mathlib/Order/Hom/Basic.lean

refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …

Modified OrderIsoClass.toOrderIso View on Github →

2023-04-13 20:39

Mathlib/Order/Hom/Basic.lean

chore: bump to nightly-2023-04-11 (#3139)

Modified OrderIsoClass.toOrderIso View on Github →

2022-12-22 21:16

Mathlib/Order/Hom/Basic.lean

feat: better coercions from hom classes to hom types (#1150) …

Added OrderIsoClass.toOrderIso View on Github →