Theorem WithZero.unzero_le_unzero

Modification history

2024-11-17 16:59
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
feat: `(WithZero α)ˣ` is isomorphic to `α` as an ordered group (#18986) …
Added WithZero.unzero_le_unzeroView on Github →