Commit 2025-02-02 08:19 702f356c

View on Github →

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

Estimated changes

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem orderOf_le_card

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem isCyclic_iff_exists_natCard_le_orderOf

added theorem isCyclic_of_card_le_orderOf