Theorem WithZero.lt_iff_exists

Modification history

2025-11-03 16:36
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
refactor: define `<` on `WithBot`/`WithTop` as an inductive predicate (#30848) …
Added WithZero.lt_iff_existsView on Github →