Theorem ArchimedeanClass.stdPart_eq

Modification history

2026-01-15 15:40
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: `r < stdPart x → r < x` (#33643)
Modified ArchimedeanClass.stdPart_eqView on Github →
2026-01-02 14:04
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: `stdPart x = sSup {r | r < x}` (#33007)
Added ArchimedeanClass.stdPart_eqView on Github →