English
Let x be a Witt vector over R and n a natural number. If the first n coefficients of x vanish, then x is equal to the n-th iterate of Verschiebung applied to x.shift n.
Русский
Пусть x — Witt-вектор над R и n — натуральное число. Если первые n коэффициентов x равны нулю, то x равно n-му повторению Verschiebung на x.shift n.
LaTeX
$$$\forall x \in \mathbb{W}_p(R), \; \forall n \in \mathbb{N}, \; (\forall i < n,\; x_i = 0) \Rightarrow x = \Verschiebung^{[n]}(x.shift\,n).$$$
Lean4
theorem eq_iterate_verschiebung {x : 𝕎 R} {n : ℕ} (h : ∀ i < n, x.coeff i = 0) : x = verschiebung^[n] (x.shift n) := by
induction n with
| zero => cases x; simp [shift]
| succ k ih =>
dsimp; rw [verschiebung_shift]
· exact ih fun i hi => h _ (hi.trans (Nat.lt_succ_self _))
· exact h
