Def CoalgHom.ofClass

Modification history

2026-09-11 08:52

Mathlib/RingTheory/Coalgebra/Hom.lean

chore: rename `Coalg{Hom,Equiv}Class.toCoalg{Hom,Equiv}` as `Coalg{Hom,Equiv}.ofClass` (#43576) …

Added CoalgHom.ofClass View on Github →