Commit 2025-06-06 21:42 d2c79fc4

View on Github →

feat(Algebra/Order/Hom/Monoid): order iso versions of unitsWithZero and friends (#22415)

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/WithZero.lean

added def MulEquiv.withZero

added def WithZero.map'

Modified Mathlib/Algebra/Order/Hom/Monoid.lean

added def OrderMonoidIso.withZero

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

added def OrderMonoidIso.withZeroUnits