coeff_one_add_X_pow — Mathlib

English

For R a semiring, the coefficient of (1 + X)^n at k is the binomial coefficient (n choose k).

Русский

Для R — полумоноидная система коэффициент (1 + X)^n при k равен биномиальному коэффициенту (n choose k).

LaTeX

$$$$\operatorname{coeff}((1 + X)^n, k) = {n \choose k}$$$$

Lean4

theorem coeff_one_add_X_pow (R : Type*) [Semiring R] (n k : ℕ) : ((1 + X) ^ n).coeff k = (n.choose k : R) := by
  rw [add_comm _ X, coeff_X_add_one_pow]

Похожие утверждения