Theorem isCyclic_iff_exists_ofOrder_eq_natCard

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) …

Deleted isCyclic_iff_exists_ofOrder_eq_natCard View on Github →

2024-04-21 11:20

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

chore(SpecificGroups/Cyclic): `Fintype` -> `Finite` (#12299)

Added isCyclic_iff_exists_ofOrder_eq_natCard View on Github →