Theorem ArchimedeanClass.exists_int_lt_of_mk_nonneg

Modification history

2026-01-08 11:26
Mathlib/Algebra/Order/Ring/Archimedean.lean
refactor: make `LinearOrderedCommMonoidWithZero`s cancellative (#31749) …
Modified ArchimedeanClass.exists_int_lt_of_mk_nonnegView on Github →
2026-01-02 14:04
Mathlib/Algebra/Order/Ring/Archimedean.lean
feat: `stdPart x = sSup {r | r < x}` (#33007)
Added ArchimedeanClass.exists_int_lt_of_mk_nonnegView on Github →