English
Let f be an R-linear map with bases b1,b2. For i in ι₂ and c in Finsupp ι₁ with finite support, the evaluation of the mv-polynomial f^{MvPolynomial}_{b1,b2}(i) at c equals the i-th coordinate of the representation of f applied to the vector given by c under b1.
Русский
Пусть f: M1 → M2 линейное. Для i∈ι₂ и c∈Finsupp ι₁ с конечной опорой, значение eval c( f.toMvPolynomial_{b1,b2}(i) ) равно i-ой координате представления f( b1.repr.symm c ).
LaTeX
$$$\\operatorname{eval}_c\\bigl(f.toMvPolynomial_{b_1,b_2}(i)\\bigr) = b_2.repr\\bigl( f\\bigl(b_1.repr.symm(c)\\bigr) \\bigr)_i$$$
Lean4
theorem toMvPolynomial_eval_eq_apply (f : M₁ →ₗ[R] M₂) (i : ι₂) (c : ι₁ →₀ R) :
eval c (f.toMvPolynomial b₁ b₂ i) = b₂.repr (f (b₁.repr.symm c)) i := by
rw [toMvPolynomial, Matrix.toMvPolynomial_eval_eq_apply, ← LinearMap.toMatrix_mulVec_repr b₁ b₂,
LinearEquiv.apply_symm_apply]
