Theorem ArchimedeanClass.lt_of_stdPart_lt

Modification history

2026-01-15 15:40
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: `r < stdPart x → r < x` (#33643)
Added ArchimedeanClass.lt_of_stdPart_ltView on Github →