English
For any natural d, the (d+1)-st power of the geometric series 1 + X + X^2 + … equals the power series whose nth coefficient is binomial(d+n, d). That is, (1 + X + X^2 + …)^{d+1} = ∑_{n≥0} binom(d+n, d) X^n.
Русский
Для любого натурального d степенной ряд 1 + X + X^2 + … в степени d+1 имеет коэффициенты в степени X равные биномиальным числам binom(d+n, d). То есть (1 + X + X^2 + …)^{d+1} = ∑_{n≥0} binom(d+n, d) X^n.
LaTeX
$$$$ \left(\sum_{n=0}^{\infty} X^n\right)^{d+1} = \sum_{n=0}^{\infty} \binom{d+n}{d} X^n $$$$
Lean4
/-- Note that `mk 1` is the constant function `1` so the power series `1 + X + X^2 + ...`. This theorem
states that for any `d : ℕ`, `(1 + X + X^2 + ... : S⟦X⟧) ^ (d + 1)` is equal to the power series
`mk fun n => Nat.choose (d + n) d : S⟦X⟧`.
-/
theorem mk_one_pow_eq_mk_choose_add : (mk 1 : S⟦X⟧) ^ (d + 1) = (mk fun n => Nat.choose (d + n) d : S⟦X⟧) := by
induction d with
| zero => ext; simp
| succ d hd =>
ext n
rw [pow_add, hd, pow_one, mul_comm, coeff_mul]
simp_rw [coeff_mk, Pi.one_apply, one_mul]
norm_cast
rw [Finset.sum_antidiagonal_choose_add, add_right_comm]
