English
Witt multiplication by n is a polynomial function in the Witt coordinates; the coeffs are computed by an algebraic expression given by wittMulN.
Русский
Умножение Witt на n — это полиномная функция по координатам Witt; коэффициенты вычисляются по выражению wittMulN.
LaTeX
$$@theorem: Witt multiplication by n is polynomial in Witt coordinates, as given by wittMulN$$
Lean4
theorem mulN_coeff (n : ℕ) (x : 𝕎 R) (k : ℕ) : (x * n).coeff k = aeval x.coeff (wittMulN p n k) := by
induction n generalizing k with
| zero => simp only [Nat.cast_zero, mul_zero, zero_coeff, wittMulN, Pi.zero_apply, map_zero]
| succ n ih =>
rw [wittMulN, Nat.cast_add, Nat.cast_one, mul_add, mul_one, aeval_bind₁, add_coeff]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
ext1 ⟨b, i⟩
fin_cases b
· simp [Function.uncurry, Matrix.cons_val_zero, ih]
· simp [Function.uncurry, Matrix.cons_val_one, aeval_X]
