Def MulEquiv.toRingEquiv

Modification history

2024-02-05 18:00

Mathlib/Algebra/Ring/Equiv.lean

refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …

Modified MulEquiv.toRingEquiv View on Github →

2023-08-10 19:52

Mathlib/Algebra/Ring/Equiv.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified MulEquiv.toRingEquiv View on Github →

2022-12-26 14:51

Mathlib/Algebra/Ring/Equiv.lean

feat: port `Algebra.Ring.Equiv` (#1077) …

Added MulEquiv.toRingEquiv View on Github →