Def ArchimedeanClass.submodule

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