Theorem OrderIso.prodComm_trans_prodUnique

Modification history

2026-11-03 04:18
Mathlib/Order/Hom/Basic.lean
feat(Order): `OrderIso.prodCongr` (#45251) …
Added OrderIso.prodComm_trans_prodUniqueView on Github →