Commit 2026-01-15 15:40 6b441804

View on Github →

feat: r < stdPart x → r < x (#33643)

Estimated changes

Modified Mathlib/Algebra/Order/Ring/StandardPart.lean

added theorem ArchimedeanClass.le_stdPart_of_le

added theorem ArchimedeanClass.lt_of_lt_stdPart

added theorem ArchimedeanClass.lt_of_stdPart_lt

modified theorem ArchimedeanClass.stdPart_eq

added theorem ArchimedeanClass.stdPart_le_of_le

added theorem ArchimedeanClass.stdPart_map_real

modified theorem ArchimedeanClass.stdPart_mul

modified theorem ArchimedeanClass.stdPart_real