Theorem RingEquiv.toRingHom_refl

Modification history

2026-09-22 13:54

Mathlib/Algebra/Ring/Equiv.lean

chore(Algebra): `coe_ringHom` -> `coe_toRingHom` (#38966)

Modified RingEquiv.toRingHom_refl View on Github →

2022-12-26 14:51

Mathlib/Algebra/Ring/Equiv.lean

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

Added RingEquiv.toRingHom_refl View on Github →