English
For R a semiring and a ∈ R, the coefficient of (X + C a)^n at k is a^{n-k} times the binomial coefficient (n choose k).
Русский
Пусть R — полусемiring и a ∈ R. Коэффициент при степени k в (X + C a)^n равен a^{n-k} C(n,k).
LaTeX
$$$$\operatorname{coeff}((X + C a)^n, k) = a^{\,n-k} \cdot {n \choose k}$$$$
Lean4
theorem coeff_X_add_C_pow (r : R) (n k : ℕ) : ((X + C r) ^ n).coeff k = r ^ (n - k) * (n.choose k : R) :=
by
rw [(commute_X (C r : R[X])).add_pow, ← lcoeff_apply, map_sum]
simp only [lcoeff_apply, ← C_eq_natCast, ← C_pow, coeff_mul_C]
rw [Finset.sum_eq_single k, coeff_X_pow_self, one_mul]
· intro _ _ h
simp [coeff_X_pow, h.symm]
· simp only [coeff_X_pow_self, one_mul, not_lt, Finset.mem_range]
intro h
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
