Theorem RingInvo.coe_ringEquiv

Modification history

2026-09-22 13:54
Mathlib/RingTheory/RingInvo.lean
chore(Algebra): `coe_ringHom` -> `coe_toRingHom` (#38966)
Deleted RingInvo.coe_ringEquivView on Github →
2023-01-27 06:03
Mathlib/RingTheory/RingInvo.lean
feat: Port RingTheory/RingInvo (#1276) …
Added RingInvo.coe_ringEquivView on Github →