Commit 2025-05-29 09:43 e88e619b

View on Github →

feat(GroupTheory/ArchimedeanDensely): type tag equivs on OrderMonoidIso (#24583) and instantiate Unique using those to prepare for unique order monoid iso on mularchimedean discrete ordered groups

Estimated changes

Modified Mathlib/Algebra/Group/Equiv/TypeTags.lean

added def AddEquiv.toAdditive_toMultiplicative

added def MulEquiv.toMultiplicative_toAdditive

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

added def OrderAddMonoidIso.toAdditive_toMultiplicative

added def OrderAddMonoidIso.toMultiplicative''

added def OrderAddMonoidIso.toMultiplicative'

added def OrderAddMonoidIso.toMultiplicative

added def OrderMonoidIso.toAdditive

added def OrderMonoidIso.toMultiplicative_toAdditive