Def AddEquiv.toMultiplicativeLeft

Modification history

2025-10-08 17:24

Mathlib/Algebra/Group/Equiv/TypeTags.lean

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

Added AddEquiv.toMultiplicativeLeft View on Github →