Theorem MulArchimedean.of_locallyFiniteOrder

Modification history

2025-07-31 11:55
Mathlib/GroupTheory/ArchimedeanDensely.lean
feat(GroupTheory/ArchimedeanDensely): locally finite linearly ordered groups are mul archimedean (#27410) …
Added MulArchimedean.of_locallyFiniteOrderView on Github →