Def MonoidHom.toAdditive'

Modification history

2024-11-22 08:58

Mathlib/Algebra/Group/TypeTags/Basic.lean

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

Modified MonoidHom.toAdditive'View on Github →

2022-12-06 01:47

Mathlib/Algebra/Group/TypeTags.lean

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

Added MonoidHom.toAdditive'View on Github →