Mathlib Changelog
v4
Changelog
About
Github
Theorem
Subgroup.isLeast_of_closure_iff_eq_mabs
Modification history
2024-09-10 16:36
Mathlib/GroupTheory/ArchimedeanDensely.lean
feat(GroupTheory/Archimedean): multiplicativize to also LinearOrderedCommGroup (#15824)
Added
Subgroup.isLeast_of_closure_iff_eq_mabs
View on Github →