Mathlib Changelog
v4
Changelog
About
Github
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