Theorem OrderIso.ofHomInv_symm_apply

Modification history

2026-03-02 11:18

Mathlib/Order/Hom/Basic.lean

refactor: make `OrderIso.ofHomInv` take actual `OrderHom`s instead of using classes (#35266)

Modified OrderIso.ofHomInv_symm_apply View on Github →

2025-07-06 01:51

Mathlib/Order/Hom/Basic.lean

feat(Order): simp lemma for applying OrderIso.ofHomInv (#26788)

Added OrderIso.ofHomInv_symm_apply View on Github →