Theorem OrderIso.orderIsoCongr_trans

Modification history

2026-11-11 00:00

Mathlib/Order/Hom/Basic.lean

chore(Order): tweak naming and simp NF of some `OrderIso`s (#45714) …

Deleted OrderIso.orderIsoCongr_trans View on Github →

2026-11-03 04:18

Mathlib/Order/Hom/Basic.lean

feat(Order): `OrderIso.prodCongr` (#45251) …

Added OrderIso.orderIsoCongr_trans View on Github →