no goals
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k in Ioo 0 p, x ^ k * y ^ (p - k) * ↑(Nat.choose p k / p)
simpa using h.add_pow_prime_pow_eq hp 1