Mathlib Changelog
v4
Changelog
About
Github
Theorem
ArchimedeanClass.stdPart_real
Modification history
2026-01-15 15:40
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: `r < stdPart x → r < x` (#33643)
Modified
ArchimedeanClass.stdPart_real
View on Github →
2025-12-17 10:18
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: standard part in non-Archimedean field (#29687) …
Added
ArchimedeanClass.stdPart_real
View on Github →