WittVector.init_isPoly

theorem WittVector.init_isPoly : ∀ (p n : ℕ), WittVector.IsPoly p fun x x_1 => WittVector.init n

The theorem `WittVector.init_isPoly` states that for every natural numbers `p` and `n`, the function that maps a Witt vector `x` to `WittVector.init n x` is a polynomial function in the coefficients of `x`. Here, `WittVector.init n x` constructs a Witt vector whose first `n` coefficients are taken from `x` and all other coefficients are `0`.

More concisely: The function mapping a Witt vector `x` to the Witt vector with its first `n` coefficients taken from `x` and all other coefficients as zero is a polynomial function in the coefficients of `x`.