init — Mathlib

English

WittVector.init n x selects the first n coefficients of x and sets all higher coefficients to zero.

Русский

WittVector.init n x оставляет первые n коэффициентов x и усекает остальные коэффициенты до нуля.

LaTeX

$$$ \text{init }(n) x = \text{select } (\lambda i. i < n) x $$$

Lean4

/-- `WittVector.init n x` is the Witt vector of which the first `n` coefficients are those from `x`
and all other coefficients are `0`.
See `WittVector.tail` for the complementary part.
-/
def init (n : ℕ) : 𝕎 R → 𝕎 R :=
  select fun i => i < n

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