Commit 2026-11-11 00:00 bfce2417

View on Github →

chore(Order): tweak naming and simp NF of some OrderIsos (#45714) ... following the post-merge comments on #45251.

Estimated changes

Modified Mathlib/Order/Hom/Basic.lean

deleted theorem OrderIso.arrowCongr_symm

deleted theorem OrderIso.orderEmbeddingCongr_symm

deleted theorem OrderIso.orderEmbeddingCongr_symm_apply

deleted theorem OrderIso.orderIsoCongr_symm

deleted theorem OrderIso.orderIsoCongr_trans

added theorem OrderIso.orderIsoCongr_trans_orderIsoCongr

added theorem OrderIso.symm_arrowCongr

added theorem OrderIso.symm_orderEmbeddingCongr

added theorem OrderIso.symm_orderIsoCongr

added theorem OrderIso.toEquiv_trans

deleted theorem OrderIso.trans_toEquiv

Modified Mathlib/Order/RelIso/Basic.lean

added theorem RelIso.relEmbeddingCongr_refl

added theorem RelIso.relEmbeddingCongr_trans_relEmbeddingCongr

added theorem RelIso.relIsoCongr_refl

added theorem RelIso.relIsoCongr_trans_relIsoCongr