Theorem ArchimedeanClass.lt_of_pos_of_archimedean

Modification history

2026-01-23 10:44
Mathlib/Algebra/Order/Ring/Archimedean.lean
feat(Analysis/Real/Hyperreal): more lemmas on `ω` and `ε` (#33649) …
Added ArchimedeanClass.lt_of_pos_of_archimedeanView on Github →