Def OrderMonoidIso.toMultiplicative_toAdditive

Modification history

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