Theorem MulArchimedeanClass.subsemigroup_eq_subgroup_of_ne_top

Modification history

2025-08-14 21:19
Mathlib/Algebra/Order/Archimedean/Class.lean
feat(Algebra/Order): ArchimedeanClass ball (#27885) …
Added MulArchimedeanClass.subsemigroup_eq_subgroup_of_ne_topView on Github →