English
If a Witt vector x is nonzero, there exists a natural number n and a Witt vector x' with a nonzero 0-th coefficient such that x equals the n-th Verschiebung iteration of x' (i.e., x = verschiebung^[n] x').
Русский
Если Witt-вектор x не равен нулю, существует n и Witt-вектор x' с не нулевым нулевым коэффициентом, такой что x = verschiebung^[n] x'.
LaTeX
$$$\forall x \in \mathbb{W}_p(R), \; x \neq 0 \Rightarrow \exists n \in \mathbb{N}, \exists x' \in \mathbb{W}_p(R), \; x'.coeff_0 \neq 0 \; \land \; x = \ Verschiebung^{[n]}(x').$$$
Lean4
theorem verschiebung_nonzero {x : 𝕎 R} (hx : x ≠ 0) : ∃ n : ℕ, ∃ x' : 𝕎 R, x'.coeff 0 ≠ 0 ∧ x = verschiebung^[n] x' :=
by
classical
have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
by_contra! hall
apply hx
ext i
simp only [hall, zero_coeff]
let n := Nat.find hex
use n, x.shift n
refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩
exact Nat.find_min hex hi
