Def AddMonoidHom.toMultiplicative''

Modification history

2025-10-08 17:24

Mathlib/Algebra/Group/TypeTags/Hom.lean

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

Deleted AddMonoidHom.toMultiplicative''View on Github →

2024-11-22 08:58

Mathlib/Algebra/Group/TypeTags/Basic.lean

chore: split Algebra.Group.TypeTags (#19351)

Modified AddMonoidHom.toMultiplicative''View on Github →

2022-12-06 01:47

Mathlib/Algebra/Group/TypeTags.lean

feat: port Algebra.Group.TypeTags (#832) …

Added AddMonoidHom.toMultiplicative''View on Github →