nthRemainder_spec — Mathlib

English

The nth remainder specification expresses the exact decomposition of (x*y)_{n+1} in terms of the level-n+1 coefficients and the truncated inputs.

Русский

Спецификация остатка n-го коэффициента точно расписывает разложение (x*y)_{n+1} через коэффициенты на уровне n+1 и усеченные входные данные.

LaTeX

$$$ (x*y)_{n+1} = x_{n+1} y_0^{p^{n+1}} + y_{n+1} x_0^{p^{n+1}} + nthRemainder\ p\ n (truncateFun(n+1)x) (truncateFun(n+1)y) $$$

Lean4

theorem nthRemainder_spec (n : ℕ) (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) +
        nthRemainder p n (truncateFun (n + 1) x) (truncateFun (n + 1) y) :=
  Classical.choose_spec (nth_mul_coeff p k n) _ _

Похожие утверждения