English
For any commutative semiring R and elements x,y ∈ R, there exists, for each n ∈ ℕ, a coefficient k ∈ R such that (x + y)^n = x^n + n x^{n−1} y + k y^2.
Русский
Для любого коммутативного полуринга R и элементов x,y ∈ R существует для каждого n ∈ ℕ коэффициент k ∈ R такой, что (x+y)^n = x^n + n x^{n−1} y + k y^2.
LaTeX
$$$\\exists k \\in R, (x+y)^n = x^n + n \\cdot x^{n-1} y + k \\cdot y^2$ для каждого n ∈ ℕ.$$
Lean4
/-- A polynomial `f` evaluated at `x + y` can be expressed as
the evaluation of `f` at `x`, plus `y` times the (polynomial) derivative of `f` at `x`,
plus some element `k : R` times `y^2`.
-/
def binomExpansion (f : R[X]) (x y : R) :
{ k : R // f.eval (x + y) = f.eval x + f.derivative.eval x * y + k * y ^ 2 } :=
by
exists f.sum fun e a => a * (polyBinomAux1 x y e a).val
rw [poly_binom_aux3]
congr
· rw [← eval_eq_sum]
· rw [derivative_eval]
exact (Finset.sum_mul ..).symm
· exact (Finset.sum_mul ..).symm
