Def OrderAddMonoidIso.toMultiplicative

Modification history

2025-07-29 04:18
Mathlib/Algebra/Order/Hom/TypeTags.lean
feat(Algebra/Order): Locally Finite Linearly Ordered Abelian Groups (#27430) …
Modified OrderAddMonoidIso.toMultiplicativeView on Github →
2025-05-29 09:43
Mathlib/GroupTheory/ArchimedeanDensely.lean
feat(GroupTheory/ArchimedeanDensely): type tag equivs on OrderMonoidIso (#24583) …
Added OrderAddMonoidIso.toMultiplicativeView on Github →