Theorem IsCyclic.exists_generator

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) …
Modified IsCyclic.exists_generatorView on Github →
2024-08-11 23:33
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
refactor(Cyclic): redefine, move definition (#15544) …
Added IsCyclic.exists_generatorView on Github →