Commit 2024-10-14 10:52 c6981000

View on Github →

refactor(CharP): make variables explicit + refactor (#14416) Follows up on Yael's comment in #8612 by making n (in x ^ (p ^ n)) explicit.

Estimated changes

modified theorem CharP.neg_one_pow_char
modified theorem CharP.neg_one_pow_char_pow
modified theorem add_pow_char
modified theorem add_pow_char_of_commute
modified theorem add_pow_char_pow
modified theorem add_pow_char_pow_of_commute
modified theorem add_pow_prime_eq
modified theorem add_pow_prime_pow_eq
modified theorem exists_add_pow_prime_eq
modified theorem exists_add_pow_prime_pow_eq
modified theorem sub_pow_char
modified theorem sub_pow_char_of_commute
modified theorem sub_pow_char_pow
modified theorem sub_pow_char_pow_of_commute