Theorem ArchimedeanClass.stdPart_nonpos

Modification history

2025-12-29 14:28
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: more lemmas on `ArchimedeanClass.stdPart` (#33343) …
Added ArchimedeanClass.stdPart_nonposView on Github →