Def AddMonoidHom.toMultiplicativeLeft

Modification history

2025-10-08 17:24

Mathlib/Algebra/Group/TypeTags/Hom.lean

chore: rename `MonoidHom.toAdditive''` to `MonoidHom.toAdditiveLeft` (#29800) …

Added AddMonoidHom.toMultiplicativeLeft View on Github →