English
There exists f such that for all x,y in Witt vectors, (x*y)_{n+1} equals a simple combination of x,y's (n+1)th components plus f on truncated inputs.
Русский
Существует f, такое что для любых Witt-векторoв x,y, (x*y)_{n+1} равно простому сочетанию компонентов (n+1) и f на усеченных входах.
LaTeX
$$$\exists f:\; TruncatedWittVector(p,n+1) \to TruncatedWittVector(p,n+1) \to k,\forall x,y, (x*y)_{n+1} = x_{n+1} y_0^{p^{n+1}} + y_{n+1} x_0^{p^{n+1}} + f( trunc(x), trunc(y) )$$$
Lean4
@[simp]
theorem bind₁_wittMulN_wittPolynomial (n k : ℕ) :
bind₁ (wittMulN p n) (wittPolynomial p ℤ k) = n * wittPolynomial p ℤ k := by
induction n with
| zero => simp [wittMulN, zero_mul, bind₁_zero_wittPolynomial]
| succ n ih =>
rw [wittMulN, ← bind₁_bind₁, wittAdd, wittStructureInt_prop]
simp only [map_add, Nat.cast_succ, bind₁_X_right]
rw [add_mul, one_mul, bind₁_rename, bind₁_rename]
simp only [ih, Function.uncurry, Function.comp_def, bind₁_X_left, AlgHom.id_apply, Matrix.cons_val_zero,
Matrix.cons_val_one]
