Def OrderIso.withTopCongr

Modification history

2025-07-11 14:29

Mathlib/Order/Hom/WithTopBot.lean

fix(Order): fix simp lemma for with{Top/Bot}{Map/Congr} (#26787) …

Modified OrderIso.withTopCongr View on Github →

2025-03-25 12:21

Mathlib/Order/Hom/Basic.lean

chore: split `Order.Hom.Lattice` (#23249) …

Modified OrderIso.withTopCongr View on Github →

2022-12-06 03:48

Mathlib/Order/Hom/Basic.lean

feat: port Order.Hom.Basic (#804) …

Added OrderIso.withTopCongr View on Github →