Commit 2026-11-03 04:18 35240244

View on Github →

feat(Order): OrderIso.prodCongr (#45251) ... and OrderIso.prodUnique, OrderIso.uniqueProd. These all follow the existing Equiv definitions.

Estimated changes

modified theorem Equiv.coe_prodUnique
modified theorem Equiv.coe_uniqueProd
modified def Equiv.prodUnique
modified theorem Equiv.prodUnique_apply
modified theorem Equiv.prodUnique_symm_apply
modified def Equiv.uniqueProd
modified theorem Equiv.uniqueProd_apply
modified theorem Equiv.uniqueProd_symm_apply
added theorem OrderIso.conj_refl
added theorem OrderIso.dual_refl
added theorem OrderIso.dual_trans
added theorem OrderIso.symm_conj
added theorem OrderIso.trans_toEquiv