Def MonoidHomClass.toMonoidHom

Modification history

2026-09-15 17:41

Mathlib/Algebra/Group/Hom/Defs.lean

chore(Algebra/MonoidHom): rename to `.ofClass` (#43755) …

Deleted MonoidHomClass.toMonoidHom View on Github →

2022-12-22 21:16

Mathlib/Algebra/Hom/Group.lean

feat: better coercions from hom classes to hom types (#1150) …

Added MonoidHomClass.toMonoidHom View on Github →