Commit 2024-02-03 14:26 0201c441

View on Github →

feat: a ^ (n % Nat.card G) = a ^ n (#10210) From LeanAPAP

Estimated changes

added theorem pow_mod_natCard
modified theorem zpow_mod_card
added theorem zpow_mod_natCard