Theorem ArchimedeanClass.top_ne_zero

Modification history

2026-01-08 11:26
Mathlib/Algebra/Order/Ring/Archimedean.lean
refactor: make `LinearOrderedCommMonoidWithZero`s cancellative (#31749) …
Modified ArchimedeanClass.top_ne_zeroView on Github →
2025-12-12 18:47
Mathlib/Algebra/Order/Ring/Archimedean.lean
feat(Algebra/Order/Ring/Archimedean): `⊤ ≠ 0` (#32800) …
Added ArchimedeanClass.top_ne_zeroView on Github →