Theorem WithZero.unzero_le_unzero

Modification history

2025-10-16 16:35
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction (#19668) …
Modified WithZero.unzero_le_unzeroView on Github →
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 →