Commit 2023-12-22 13:04 c54f3fb4

View on Github →

feat: 1 is the only positive element of finite order (#9110) and other simple lemmas about the order of elements in a group From LeanAPAP

Estimated changes

added theorem IsOfFinOrder.pow
deleted theorem pow_eq_mod_card
added theorem pow_mod_card
deleted theorem zpow_eq_mod_card
added theorem zpow_mod_card