verschiebungFun_coeff — Mathlib

English

For any Witt vector x and any n, the n-th coefficient of verschiebungFun x is 0 if n = 0, otherwise it equals x.coeff(n−1).

Русский

Для любого вита x и любого n-й коэффициент verschiebungFun x равен 0, если n=0, иначе он равен x.coeff(n−1).

LaTeX

$$$$ (\\\\text{verschiebungFun}(x))_n = \\begin{cases}0, & n=0 \\\\ x_{n-1}, & n>0\\end{cases} $$$$

Lean4

theorem verschiebungFun_coeff (x : 𝕎 R) (n : ℕ) : (verschiebungFun x).coeff n = if n = 0 then 0 else x.coeff (n - 1) :=
  by simp only [verschiebungFun]

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