Mathlib Changelog
v4
Changelog
About
Github
Theorem
Subgroup.dense_iff_not_isCyclic
Modification history
2026-10-07 11:50
Mathlib/Topology/Algebra/Order/ArchimedeanDiscrete.lean
chore(GroupTheory/Archimedean): spell cyclic results using `IsCyclic` (#43245) …
Added
Subgroup.dense_iff_not_isCyclic
View on Github →