Theorem WithZero.lt_iff_exists_coe

Modification history

2025-10-16 16:35
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction (#19668) …
Added WithZero.lt_iff_exists_coeView on Github →