Theorem AddMonoidHom.coe_toMultiplicativeRight

Modification history

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