Def OrderIso.withZeroUnits

Modification history

2025-07-09 21:00
Mathlib/Algebra/Order/GroupWithZero/WithZero.lean
chore(Order/WithZero): `OrderIso.withZeroUnits` (#26940) …
Added OrderIso.withZeroUnitsView on Github →