toMvPolynomial_eval_eq_apply — Mathlib

English

For a matrix M, the scalar evaluation of its mv-polynomial representation at c equals the i-th entry of the matrix-vector product M c; i.e., eval_c(M.toMvPolynomial i) = (M *ᵥ c)_i.

Русский

Для матрицы M оценка mv-полинома вектора c даёт i-ю компоненту произведения матрица-вектор: eval_c(M.toMvPolynomial i) = (M *ᵥ c)_i.

LaTeX

$$eval_c(M.toMvPolynomial i) = (M *ᵥ c)_i$$

Lean4

theorem toMvPolynomial_eval_eq_apply (M : Matrix m n R) (i : m) (c : n → R) :
    eval c (M.toMvPolynomial i) = (M *ᵥ c) i := by
  simp only [toMvPolynomial, map_sum, eval_monomial, pow_zero, Finsupp.prod_single_index, pow_one, mulVec, dotProduct]

Похожие утверждения