Def OrderAddMonoidIso.toMultiplicative''

Modification history

2025-10-08 17:24

Mathlib/Algebra/Order/Hom/TypeTags.lean

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

Deleted OrderAddMonoidIso.toMultiplicative''View on Github →

2025-07-29 04:18

Mathlib/Algebra/Order/Hom/TypeTags.lean

feat(Algebra/Order): Locally Finite Linearly Ordered Abelian Groups (#27430) …

Modified OrderAddMonoidIso.toMultiplicative''View on Github →

2025-05-29 09:43

Mathlib/GroupTheory/ArchimedeanDensely.lean

feat(GroupTheory/ArchimedeanDensely): type tag equivs on OrderMonoidIso (#24583) …

Added OrderAddMonoidIso.toMultiplicative''View on Github →