English
Let M be an m×n matrix over R and N an n×o matrix over R. Then the multivariate polynomial associated to the product M N at index i equals the bound-1 composition of the multivariate polynomials of N with the i-th polynomial of M: (M N).toMvPolynomial i = bind₁ N.toMvPolynomial (M.toMvPolynomial i).
Русский
Пусть M — матрица размером m×n, а N — матрица размером n×o над кольцом R. Тогда mv-полином, соответствующий произведению M N в координате i, равен консеквенции подстановки: (M N).toMvPolynomial i = bind₁ N.toMvPolynomial (M.toMvPolynomial i).
LaTeX
$$$ (M N).toMvPolynomial i = \\operatorname{bind}_1\\left(N.toMvPolynomial\\right)\\left(M.toMvPolynomial i\\right) $$$
Lean4
theorem toMvPolynomial_mul (M : Matrix m n R) (N : Matrix n o R) (i : m) :
(M * N).toMvPolynomial i = bind₁ N.toMvPolynomial (M.toMvPolynomial i) := by
simp only [toMvPolynomial, mul_apply, map_sum, Finset.sum_comm (γ := o), bind₁, aeval, AlgHom.coe_mk, coe_eval₂Hom,
eval₂_monomial, algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply, C_apply, pow_zero,
Finsupp.prod_single_index, pow_one, Finset.mul_sum, monomial_mul, zero_add]
