Commit 2025-12-04 21:34 25333c50
View on Github →fix: correct RingEquiv.ofHomInv so that it doesn't use RingHomClass (#32361)
Per #mathlib4 > Mathlib's morphism hierarchy, this removes the use of coercions from RingHomClass in the construction RingEquiv.ofHomInv.