English
For every n, the product with polyOfInterest scaled by p^{n+1} equals the remainder minus the Witt remainder term. This isolates the part of polyOfInterest contributing to higher Witt coefficients from the remainders.
Русский
Для каждого n произведение, связанное с polyOfInterest и умноженное на p^{n+1}, равно остатку минус члену остатка Witt. Так выделяется часть polyOfInterest, вносящая вклад в более высокие коэффициенты Witt, отделенная в остатке.
LaTeX
$$$(p^{n+1}) \cdot polyOfInterest\ p\ n = remainder\ p\ n - wittPolyProdRemainder\ p\ (n+1)$$$
Lean4
theorem mul_polyOfInterest_aux5 (n : ℕ) :
(p : 𝕄) ^ (n + 1) * polyOfInterest p n = remainder p n - wittPolyProdRemainder p (n + 1) :=
by
simp only [polyOfInterest, mul_sub, mul_add, sub_eq_iff_eq_add']
rw [mul_polyOfInterest_aux4 p n]
ring
