Skip to content

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

e4193e7
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
Closed

[Merged by Bors] - feat: more lemmas on ArchimedeanClass.stdPart #33343

Update Mathlib/Algebra/Order/Ring/StandardPart.lean
e4193e7
Select commit
Loading
Failed to load commit list.
Lint style (fork)
succeeded Dec 28, 2025 in 2m 7s