Theorem ArchimedeanClass.mk_le_mk_smul

Modification history

2025-09-01 13:46
Mathlib/Algebra/Order/Module/Archimedean.lean
feat(Algebra/Order): ArchimedeanClass ball for module (#28449) …
Added ArchimedeanClass.mk_le_mk_smulView on Github →