Commit 2026-09-15 17:41 53634212
View on Github →chore(Algebra/MonoidHom): rename to .ofClass (#43755)
Following #mathlib4 > Mathlib's morphism hierarchy item 2, rename MonoidHomClass.toMonoidHom to MonoidHom.ofClass.
Lemmas with name coe_monoidHom_foo and coe_addMonoidHom_foo (related to simp normal form) are temporarily renamed to ofClass_monoidHom_foo and ofClass_addMonoidHom_foo. They will be renamed to toMonoidHom_foo toAddMonoidHom_foo once we moved the coe from .ofClass f to f.toMonoidHom.
This is in parallel with #43611 (refactoring definitions from taking MonoidHomClass to taking MonoidHom).