English
Over ZMod(p^(n+1)), the (n+1)-st Witt polynomial equals the expansion by p of the n-th Witt polynomial.
Русский
В ZMod(p^(n+1)) н-ая полином Витта выражает через разложение на степень p предыдущего полинома.
LaTeX
$$$W_{(n+1)}^{\mathbb{Z}/p^{n+1}} = \mathrm{expand}_p\big(W_n^{\mathbb{Z}/p^{n+1}}\big)$$$
Lean4
/-- Over the ring `ZMod (p^(n+1))`, we produce the `n+1`st Witt polynomial
by expanding the `n`th Witt polynomial by `p`. -/
@[simp]
theorem wittPolynomial_zmod_self (n : ℕ) : W_ (ZMod (p ^ (n + 1))) (n + 1) = expand p (W_ (ZMod (p ^ (n + 1))) n) :=
by
simp only [wittPolynomial_eq_sum_C_mul_X_pow]
rw [sum_range_succ, ← Nat.cast_pow, CharP.cast_eq_zero (ZMod (p ^ (n + 1))) (p ^ (n + 1)), C_0, zero_mul, add_zero,
map_sum, sum_congr rfl]
intro k hk
rw [map_mul (expand p), map_pow (expand p), expand_X, algHom_C, ← pow_mul, ← pow_succ']
congr
rw [mem_range] at hk
rw [add_comm, add_tsub_assoc_of_le (Nat.lt_succ_iff.mp hk), ← add_comm]
