apply_eq_pow_smul_coeff — Mathlib

English

Let p be a formal multilinear series with coefficients coeff n. For every n ∈ ℕ and z ∈ 𝕜, the nth term evaluated at the constant input z, i.e. (p n)(λ i. z), equals z^n times the nth coefficient: (p n)(λ i. z) = z^n · (coeff p n).

Русский

Пусть p — формальная мультилейнерная серия с коэффициентами coeff n. Для каждого n ∈ ℕ и z ∈ 𝕜 выражение $ (p n)(λ i. z) $ равно $ z^n $ умножить на коэффициент $ coeff p n $: (p n)(λ i. z) = z^n · (coeff p n).

LaTeX

$$$ (p\,n)(\\lambda i. z) = z^{n} \\cdot (p.coeff\\, n) $$$

Lean4

theorem apply_eq_pow_smul_coeff : (p n fun _ => z) = z ^ n • p.coeff n := by simp

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