aeval_verschiebung_poly' — Mathlib

English

For any x and n, evaluating the VerschiebungPoly(n) under the coefficient algebra of x yields the n-th coefficient of verschiebungFun x.

Русский

Для любого x и n, применение aeval к verschiebungPoly(n) по коэффициентам x дает n-й коэффициент verschiebungFun x.

LaTeX

$$$$ \\mathrm{aeval}(x.\\\\coeff, \\\\mathrm{verschiebungPoly}(n)) = (\\\\text{verschiebungFun}(x)).coeff(n). $$$$

Lean4

theorem aeval_verschiebung_poly' (x : 𝕎 R) (n : ℕ) : aeval x.coeff (verschiebungPoly n) = (verschiebungFun x).coeff n :=
  by
  rcases n with - | n
  · simp only [verschiebungPoly, ite_true, map_zero, verschiebungFun_coeff_zero]
  · rw [verschiebungPoly, verschiebungFun_coeff_succ, if_neg n.succ_ne_zero, aeval_X, add_tsub_cancel_right]

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