Def MonoidHom.toAdditiveLeft

Modification history

2025-10-08 17:24

Mathlib/Algebra/Group/TypeTags/Hom.lean

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

Added MonoidHom.toAdditiveLeft View on Github →