Theorem RingEquiv.symm_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.symm_ofNonUnitalRingHomView on Github →