Def AddMonoidHom.toMultiplicative'

Modification history

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 →