Theorem ArchimedeanClass.ball_le_closedBall

Modification history

2026-07-15 16:59
Mathlib/Algebra/Order/Module/Archimedean.lean
chore: delete deprecated declarations to the end of 2025 (#41178) …
Deleted ArchimedeanClass.ball_le_closedBallView on Github →
2025-09-09 14:11
Mathlib/Algebra/Order/Module/Archimedean.lean
feat(Algebra/Order): ArchimedeanClass.ball ≤ .closedBall (#29423) …
Added ArchimedeanClass.ball_le_closedBallView on Github →