Theorem isCyclic_iff_exists_zpowers_eq_top

Modification history

2024-12-20 11:24

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

refactor(GroupTheory/SpecificGroups/Cyclic): Add `isCyclic_iff_exists_zpowers_eq_top` and golf (#20085) …

Added isCyclic_iff_exists_zpowers_eq_top View on Github →