English
For k ∈ N, a1, a2 ∈ A, p1, p2 ∈ R[X], the product of coefficients across p1 and p2 equals the sum over the antidiagonal of k of certain products involving a1, a2 and the coefficients of p1 and p2.
Русский
Для k ∈ N, a1, a2 ∈ A, p1, p2 ∈ R[X], произведение коэффициентов через p1 и p2 равняется сумме по антидиагонали k от соответствующих произведений, включающих a1, a2 и коэффициенты p1, p2.
LaTeX
$$$a_1 a_2 \\cdot \\mathrm{algebraMap}_R^A( (p_1 p_2).\\mathrm{coeff}\\ k ) = \\sum_{x \\in \\mathrm{antidiagonal}(k)} a_1 \\cdot \\mathrm{algebraMap}_R^A(p_1(x.1)) \\cdot (a_2 \\cdot \\mathrm{algebraMap}_R^A(p_2(x.2)))$$$
Lean4
theorem toFunLinear_mul_tmul_mul_aux_2 (k : ℕ) (a₁ a₂ : A) (p₁ p₂ : R[X]) :
a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) =
(Finset.antidiagonal k).sum fun x =>
a₁ * (algebraMap R A) (coeff p₁ x.1) * (a₂ * (algebraMap R A) (coeff p₂ x.2)) :=
by
simp_rw [mul_assoc, Algebra.commutes, ← Finset.mul_sum, mul_assoc, ← Finset.mul_sum]
congr
simp_rw [Algebra.commutes (coeff p₂ _), coeff_mul, map_sum, RingHom.map_mul]
