English
There exists a bilinear map f such that the (n+1)st coefficient of the product x*y equals the sum of specific contributions, separating the main product from tail terms captured by f.
Русский
Существует билинейная карта f, такая что (x*y)_{n+1} равен сумме конкретных вкладов, отделяющей главную часть произведения от хвоста, отраженного f.
LaTeX
$$$\exists f:\, TruncatedWittVector(p,n+1)\to TruncatedWittVector(p,n+1)\to k,\forall x,y:\mathbb{W}^k,\ (x*y)_{n+1} = x_{n+1} y_0^{p^{n+1}} + y_{n+1} x_0^{p^{n+1}} + f(\operatorname{truncateFun}(n+1,x),\operatorname{truncateFun}(n+1,y))$$$
Lean4
theorem nth_mul_coeff (n : ℕ) :
∃ f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k,
∀ x y : 𝕎 k,
(x * y).coeff (n + 1) =
x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
f (truncateFun (n + 1) x) (truncateFun (n + 1) y) :=
by
obtain ⟨f, hf⟩ := nth_mul_coeff' p k n
use f
intro x y
rw [hf x y]
ring
