Coefficients of powers of linear polynomials #
The binomial coefficient formula for (a + b X)^n allows coefficient calculations without
expanding a polynomial into a finite sum at each use.
@[simp]
theorem
TauCeti.coeff_C_add_C_mul_X_pow
{R : Type u_1}
[CommSemiring R]
(a b : R)
(n k : ℕ)
:
((Polynomial.C a + Polynomial.C b * Polynomial.X) ^ n).coeff k = ↑(n.choose k) * a ^ (n - k) * b ^ k
The coefficient of X^k in (a + b X)^n, including coefficients above the degree.