Commit 2023-04-01 16:09 b38baa7d

View on Github →

chore: re-port Algebra.CharP.Basic (#3191) This forward-ports changes from leanprover-community/mathlib#11364 One unrelated downstream file times out, presumably due to the import graph subtly changing.

Estimated changes

Modified Mathlib/Algebra/CharP/Basic.lean

modified theorem add_pow_char_of_commute

modified theorem add_pow_char_pow_of_commute

added theorem add_pow_prime_eq

added theorem add_pow_prime_pow_eq

added theorem exists_add_pow_prime_eq

added theorem exists_add_pow_prime_pow_eq

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean