Theorem AddMonoidHom.coe_toMultiplicativeLeft

Modification history

2025-10-08 17:24
Mathlib/Algebra/Group/TypeTags/Hom.lean
chore: rename `MonoidHom.toAdditive''` to `MonoidHom.toAdditiveLeft` (#29800) …
Added AddMonoidHom.coe_toMultiplicativeLeftView on Github →