Theorem RelIso.relEmbeddingCongr_trans_relEmbeddingCongr

Modification history

2026-11-11 00:00
Mathlib/Order/RelIso/Basic.lean
chore(Order): tweak naming and simp NF of some `OrderIso`s (#45714) …
Added RelIso.relEmbeddingCongr_trans_relEmbeddingCongrView on Github →