Def AddEquiv.toMultiplicativeRight

Modification history

2026-09-10 14:29

Mathlib/Algebra/Group/Equiv/TypeTags.lean

chore(Algebra/Group/Equiv/TypeTags): generalize to `Add` and `Mul` and deprecate duplicates (#43661) …

Modified AddEquiv.toMultiplicativeRight View on Github →

2025-10-08 17:24

Mathlib/Algebra/Group/Equiv/TypeTags.lean

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

Added AddEquiv.toMultiplicativeRight View on Github →