Commit 2024-01-10 14:23 eee12691

View on Github →

feat: a * a ^ (n - 1) = a ^ n (#9610) From LeanAPAP

Estimated changes

added theorem mul_pow_sub_one
added theorem pow_sub_one_mul
modified theorem pow_succ'