Def RingInvoClass.toRingInvo

Modification history

2024-02-05 18:00
Mathlib/RingTheory/RingInvo.lean
refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …
Modified RingInvoClass.toRingInvoView on Github →
2023-01-27 06:03
Mathlib/RingTheory/RingInvo.lean
feat: Port RingTheory/RingInvo (#1276) …
Added RingInvoClass.toRingInvoView on Github →