Binomial theorem

import Mathlib

theorem binomial_thm {R : Type*} [CommSemiring R] (x y : R) (n : ℕ) : (x + y) ^ n = ∑ k ∈ Finset.range (n + 1), Nat.choose n k * x ^ k * y ^ (n - k) := by
  rw [add_pow]
  congr 1
  ext k
  ring