Commit 2025-09-01 13:46 88a075ca

feat(Algebra/Order): ArchimedeanClass ball for module (#28449) This continues #27885 and promotes ArchimedeanClass.addSubgroup to a submodule. Balls are promoted to submodules with shorter names ball and closedBall, as they will be used a lot in the proof of Hahn embedding theorem (if you don't agree with this I can rename them to ballSubmodule and closedBallSubmodule)