English
A key decomposition shows that a certain finite sum equals the Witt polynomial product wittPolyProd p n.
Русский
Ключевое разложение показывает, что некоторое конечное суммирование равно произведению Witt-полиномов wittPolyProd p n.
LaTeX
$$$\sum_{i=0}^{n} p^{i} wittMul(p,i)^{p^{(n-i)}} = wittPolyProd(p,n).$$$
Lean4
theorem mul_polyOfInterest_aux1 (n : ℕ) :
∑ i ∈ range (n + 1), (p : 𝕄) ^ i * wittMul p i ^ p ^ (n - i) = wittPolyProd p n :=
by
simp only [wittPolyProd]
convert wittStructureInt_prop p (X (0 : Fin 2) * X 1) n using 1
· simp only [wittPolynomial, wittMul]
rw [map_sum]
congr 1 with i
congr 1
have hsupp : (Finsupp.single i (p ^ (n - i))).support = { i } :=
by
rw [Finsupp.support_eq_singleton]
simp only [and_true, Finsupp.single_eq_same, Ne]
exact pow_ne_zero _ hp.out.ne_zero
simp only [bind₁_monomial, hsupp, Int.cast_natCast, prod_singleton, eq_intCast, Finsupp.single_eq_same,
Int.cast_pow]
· simp only [map_mul, bind₁_X_right]
