English
Iterating Verschiebung, after surpassing n steps, yields zero at coefficient m when m < n.
Русский
Итерируя Verschiebung, после более чем n шагов, коэффициент m становится нулём при m < n.
LaTeX
$$$ (verschiebung^{[n]} x).coeff m = 0 \quad \text{for } m < n $$$
Lean4
/-- This is a slightly specialized form of [Hazewinkel, *Witt Vectors*][Haze09] 6.2 equation 5. -/
theorem iterate_verschiebung_mul_coeff (x y : 𝕎 R) (i j : ℕ) :
(verschiebung^[i] x * verschiebung^[j] y).coeff (i + j) = x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i :=
by
calc
_ = (verschiebung^[i + j] (frobenius^[j] x * frobenius^[i] y)).coeff (i + j) := ?_
_ = (frobenius^[j] x * frobenius^[i] y).coeff 0 := ?_
_ = (frobenius^[j] x).coeff 0 * (frobenius^[i] y).coeff 0 := ?_
_ = _ := ?_
· rw [iterate_verschiebung_mul]
· convert iterate_verschiebung_coeff (p := p) (R := R) _ _ _ using 2
rw [zero_add]
· apply mul_coeff_zero
· simp only [iterate_frobenius_coeff]
