Theorem ArchimedeanClass.stdPart_of_mk_ne_zero

Modification history

2025-12-24 17:12
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: more theorems on `ArchimedeanClass.stdPart` (#33048)
Deleted ArchimedeanClass.stdPart_of_mk_ne_zeroView on Github →
2025-12-17 10:18
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: standard part in non-Archimedean field (#29687) …
Added ArchimedeanClass.stdPart_of_mk_ne_zeroView on Github →