shift — Mathlib

English

Shift of a Witt vector by n reindexes its components: the k-th coefficient of shift(x,n) equals x.coeff(n+k).

Русский

Сдвиг Witt-вектора на n переиндексирует его компоненты: k-й коэффициент shift(x,n) равен x.coeff(n+k).

LaTeX

$$$(\text{shift}(x,n)).\text{coeff } k = x.\text{coeff }(n+k)$$$

Lean4

/-- `WittVector.verschiebung` translates the entries of a Witt vector upward, inserting 0s in the gaps.
`WittVector.shift` does the opposite, removing the first entries.
This is mainly useful as an auxiliary construction for `WittVector.verschiebung_nonzero`.
-/
def shift (x : 𝕎 R) (n : ℕ) : 𝕎 R :=
  @mk' p R fun i => x.coeff (n + i)

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