Prime_Power_of_Sum_Modulo_Prime
Provednumber-theoryprime-numbersproofwiki
For prime p: (a+b)^(p^n) ≡ a^(p^n) + b^(p^n) (mod p).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Prime_Power_of_Sum_Modulo_Prime (p : ℕ) (hp : Nat.Prime p) (a b : ℤ) (n : ℕ) (hn : 0 < n) : ((a + b) ^ p ^ n - (a ^ p ^ n + b ^ p ^ n)) % p = 0 := by sorry
Source