Def RingEquiv.ofNonUnitalRingHom

Modification history

2025-12-04 21:34

Mathlib/Algebra/Ring/Equiv.lean

fix: correct `RingEquiv.ofHomInv` so that it doesn't use `RingHomClass` (#32361) …

Added RingEquiv.ofNonUnitalRingHom View on Github →