Commit 2024-12-20 11:24 a7ed2d05

View on Github →

refactor(GroupTheory/SpecificGroups/Cyclic): Add isCyclic_iff_exists_zpowers_eq_top and golf (#20085) This PR adds isCyclic_iff_exists_zpowers_eq_top and does a little golfing.

Estimated changes

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

modified theorem IsCyclic.exists_generator

deleted theorem isCyclic_iff_exists_ofOrder_eq_natCard

added theorem isCyclic_iff_exists_orderOf_eq_natCard

added theorem isCyclic_iff_exists_zpowers_eq_top