Theorem WithZero.withZeroUnitsEquiv_strictMono

Modification history

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