Theorem ArchimedeanClass.toAddSubgroup_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.toAddSubgroup_closedBallView on Github →
2025-09-01 13:46
Mathlib/Algebra/Order/Module/Archimedean.lean
feat(Algebra/Order): ArchimedeanClass ball for module (#28449) …
Added ArchimedeanClass.toAddSubgroup_closedBallView on Github →