English
The algebraic equality shows that applying the rename-expanded Witt polynomial to wittMulN yields the expected multiplication by n, reflecting the linearity in the Witt coefficient expansion.
Русский
Алгебраическое равенство показывает, что применение переименованного расширенного Witt-полинома к wittMulN даёт ожидаемое умножение на n, отражая линейность разложения по Witt-коэффициентам.
LaTeX
$$$\bind₁ (wittMulN\ p\ n) (wittPolynomial\ p\ ℤ\ k) = n * wittPolynomial\ p\ ℤ\ k$$$
Lean4
theorem wittStructureRat_rec_aux (Φ : MvPolynomial idx ℚ) (n : ℕ) :
wittStructureRat p Φ n * C ((p : ℚ) ^ n) =
bind₁ (fun b => rename (fun i => (b, i)) (W_ ℚ n)) Φ -
∑ i ∈ range n, C ((p : ℚ) ^ i) * wittStructureRat p Φ i ^ p ^ (n - i) :=
by
have := xInTermsOfW_aux p ℚ n
replace := congr_arg (bind₁ fun k : ℕ => bind₁ (fun i => rename (Prod.mk i) (W_ ℚ k)) Φ) this
rw [map_mul, bind₁_C_right] at this
rw [wittStructureRat, this]; clear this
conv_lhs => simp only [map_sub, bind₁_X_right]
rw [sub_right_inj]
simp only [map_sum, map_mul, bind₁_C_right, map_pow]
rfl
