Theorem isCyclic_iff_exists_natCard_le_orderOf

Modification history

2025-02-02 08:19

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

chore(GroupTheory/SpecificGroups/Cyclic): isCyclic_of_card_le_orderOf (#21297)

Added isCyclic_iff_exists_natCard_le_orderOf View on Github →