Commit 2025-07-09 21:00 97e6e357

View on Github →

chore(Order/WithZero): OrderIso.withZeroUnits (#26940) not bundled because Algebra/Order/GroupWithZero/WithZero.lean doesn't import OrderMonoidIso and move OrderMonoidIso.withZeroUnits earlier

Estimated changes

Modified Mathlib/Algebra/Order/GroupWithZero/WithZero.lean

added def OrderIso.withZeroUnits

added theorem WithZero.withZeroUnitsEquiv_strictMono

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

added def OrderMonoidIso.withZeroUnits

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

deleted def OrderMonoidIso.withZeroUnits