Def RingEquiv.ringEquivOfUnique

Modification history

2024-12-27 11:03
Mathlib/Algebra/Ring/Equiv.lean
chore: rename `MulEquiv.mulEquivOfUnique` to `MulEquiv.ofUnique` (#20243)
Deleted RingEquiv.ringEquivOfUniqueView on Github →
2022-12-26 14:51
Mathlib/Algebra/Ring/Equiv.lean
feat: port `Algebra.Ring.Equiv` (#1077) …
Added RingEquiv.ringEquivOfUniqueView on Github →