aeval_verschiebungPoly — Mathlib

English

For all p and R, and x ∈ 𝕎R, and n, the evaluation of verschiebungPoly(n) at x’s coefficients equals the nth coefficient of verschiebung x.

Русский

Для всех p и R и x ∈ 𝕎R и n, вычисление VerschiebungPoly(n) в коэффициентах x равно n-ому коэффициенту verschiebung x.

LaTeX

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

Lean4

theorem aeval_verschiebungPoly (x : 𝕎 R) (n : ℕ) : aeval x.coeff (verschiebungPoly n) = (verschiebung x).coeff n :=
  aeval_verschiebung_poly' x n

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