English
Let R be a commutative ring and x be a Witt vector over R. The tail operator tail(n) returns the Witt vector whose first n coefficients are zero and whose remaining coefficients are those of x.
Русский
Пусть R — коммутативное кольцо, а x — Witt-вектор над R. Оператор tail(n) возвращает Witt-вектор, в котором первые n коэффициентов равны нулю, а остальные равны соответствующим коэффициентам x.
LaTeX
$$$$(\operatorname{tail}(n) x)_i = \begin{cases}0, & i < n \\ x_i, & i \ge n\end{cases}$$$$
Lean4
/-- `WittVector.tail n x` is the Witt vector of which the first `n` coefficients are `0`
and all other coefficients are those from `x`.
See `WittVector.init` for the complementary part. -/
def tail (n : ℕ) : 𝕎 R → 𝕎 R :=
select fun i => n ≤ i
