binomialSeries_nat — Mathlib

English

For d ∈ N, binomialSeries A d (cast) equals (1 + X)^d as a power series.

Русский

Для натурального d биномиальный ряд при d равен $(1+X)^d$ как ряд степенных.

LaTeX

$$$\\text{binomialSeries } A (d: \\mathbb{N}) = (1 + X)^d$$$

Lean4

@[simp]
theorem binomialSeries_nat [Ring A] [Algebra R A] (d : ℕ) : binomialSeries A (d : R) = (1 + X) ^ d :=
  by
  ext n
  have hright : (1 + X) ^ d = (((1 : Polynomial A) + (Polynomial.X)) ^ d).toPowerSeries := by simp
  rw [hright, Polynomial.coeff_coe, binomialSeries_coeff, Polynomial.coeff_one_add_X_pow]
  simp [Ring.choose_natCast, Nat.cast_smul_eq_nsmul]

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