binomialSeries_add — Mathlib

English

The binomial series is multiplicative in the exponent: binomialSeries A (r + s) = binomialSeries A r · binomialSeries A s.

Русский

Биномиальный ряд умножается по сложению степеней: binomialSeries A (r + s) = binomialSeries A r · binomialSeries A s.

LaTeX

$$$\\text{binomialSeries } A (r + s) = \\text{binomialSeries } A r \\cdot \\text{binomialSeries } A s$$$

Lean4

@[simp]
theorem binomialSeries_add [Ring A] [Algebra R A] (r s : R) :
    binomialSeries A (r + s) = binomialSeries A r * binomialSeries A s :=
  by
  ext n
  simp only [binomialSeries_coeff, Ring.add_choose_eq n (Commute.all r s), coeff_mul, Algebra.mul_smul_comm, mul_one,
    sum_smul]
  refine sum_congr rfl fun ab hab => ?_
  rw [mul_comm, mul_smul]

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