Commit 2025-12-29 14:28 7edc8dd2

View on Github →

feat: more lemmas on ArchimedeanClass.stdPart (#33343) Upstreamed from the CGT repo.

Estimated changes

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

deleted theorem ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk'

added theorem ArchimedeanClass.stdPart_nonneg

added theorem ArchimedeanClass.stdPart_nonpos