English
A further expansion of wittPolyProd p (n+1) expresses it as a combination of X-terms, renamed Witt polynomials, and the remainder.
Русский
Далее разложение wittPolyProd p (n+1) выражает его через X-термы, переименованные Witt-полиномы и остаток.
LaTeX
$$$\text{wittPolyProd}(p,n+1)= -p^{n+1}X(0,n+1)\cdot p^{n+1}X(1,n+1) + p^{n+1}X(0,n+1)\text{rename}(...)+ p^{n+1}X(1,n+1)\text{rename}(...)+\text{remainder}(p,n).$$$
Lean4
theorem mul_polyOfInterest_aux3 (p n : ℕ) :
wittPolyProd p (n + 1) =
-((p : 𝕄) ^ (n + 1) * X (0, n + 1)) * ((p : 𝕄) ^ (n + 1) * X (1, n + 1)) +
(p : 𝕄) ^ (n + 1) * X (0, n + 1) * rename (Prod.mk (1 : Fin 2)) (wittPolynomial p ℤ (n + 1)) +
(p : 𝕄) ^ (n + 1) * X (1, n + 1) * rename (Prod.mk (0 : Fin 2)) (wittPolynomial p ℤ (n + 1)) +
remainder p n :=
by
-- a useful auxiliary fact
have mvpz : (p : 𝕄) ^ (n + 1) = MvPolynomial.C ((p : ℤ) ^ (n + 1)) := by norm_cast
rw [wittPolyProd, wittPolynomial, map_sum, map_sum]
conv_lhs =>
arg 1
rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
conv_lhs =>
arg 2
rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
conv_rhs =>
enter [1, 1, 2, 2]
rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
conv_rhs =>
enter [1, 2, 2]
rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
simp only [add_mul, mul_add]
rw [add_comm _ (remainder p n)]
simp only [add_assoc]
apply congrArg (Add.add _)
ring
