Theorem OrderIso.orderEmbeddingCongr_symm_apply

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.orderEmbeddingCongr_symm_applyView on Github →
2026-06-25 15:32
Mathlib/Order/Hom/Basic.lean
feat(Order/Hom/Basic): equivalences of `Order{Hom/Embedding/Iso}` (#38667) …
Added OrderIso.orderEmbeddingCongr_symm_applyView on Github →