Commit 2026-03-02 11:18 9fd7e6df

View on Github →

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

Estimated changes

Modified Mathlib/Order/Hom/Basic.lean

modified def OrderIso.ofHomInv

modified theorem OrderIso.ofHomInv_symm_apply

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean