Commit 2025-09-09 14:11 78ec5ad6
View on Github →feat(Algebra/Order): ArchimedeanClass.ball ≤ .closedBall (#29423) One missing lemma that will be used in #27268 Hahn embedding theorem
feat(Algebra/Order): ArchimedeanClass.ball ≤ .closedBall (#29423) One missing lemma that will be used in #27268 Hahn embedding theorem