coeff_eval_eq_eval_coeff — Mathlib

English

For any s' : S1 → R, f ∈ Polynomial(MvPolynomial S1 R), and i, the coefficient of i in the map of f by eval s' equals eval s' applied to the i-th coefficient of f.

Русский

Для любой функции s', f и i коэффициент i в отображении через map равен eval s' применённому к коэффициенту f на i.

LaTeX

$$$\\operatorname{Polynomial}.coeff(\\operatorname{Polynomial}.map(\\operatorname{eval} s')\n f)\\; i = \\operatorname{eval} s' (f.\\coeff i)$$$

Lean4

theorem coeff_eval_eq_eval_coeff (s' : S₁ → R) (f : Polynomial (MvPolynomial S₁ R)) (i : ℕ) :
    Polynomial.coeff (Polynomial.map (eval s') f) i = eval s' (Polynomial.coeff f i) := by
  simp only [Polynomial.coeff_map]

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