Def OrderIsoClass.toOrderIso

Modification history

2026-09-07 13:06
Mathlib/Order/Hom/Basic.lean
chore: standardise names for coercions from morphism classes to morphisms (#43367) …
Deleted OrderIsoClass.toOrderIsoView on Github →
2024-02-05 18:00
Mathlib/Order/Hom/Basic.lean
refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …
Modified OrderIsoClass.toOrderIsoView on Github →
2023-04-13 20:39
Mathlib/Order/Hom/Basic.lean
chore: bump to nightly-2023-04-11 (#3139)
Modified OrderIsoClass.toOrderIsoView on Github →
2022-12-22 21:16
Mathlib/Order/Hom/Basic.lean
feat: better coercions from hom classes to hom types (#1150) …
Added OrderIsoClass.toOrderIsoView on Github →