English
Evaluating the mvPolynomialX matrix by a polynomial evaluation map recovers the original matrix A: the map sends mvPolynomialX evaluated at A entries to A.
Русский
Применение mvPolynomialX к матрице A через отображение eval₂ возвращает исходную матрицу A.
LaTeX
$$$(mvPolynomialX_{m,n,R}).map (MvPolynomial.eval_2 f\, (\lambda p: A\,p.1\,p.2)) = A$$$
Lean4
/-- Any matrix `A` can be expressed as the evaluation of `Matrix.mvPolynomialX`.
This is of particular use when `MvPolynomial (m × n) R` is an integral domain but `S` is
not, as if the `MvPolynomial.eval₂` can be pulled to the outside of a goal, it can be solved in
under cancellative assumptions. -/
theorem mvPolynomialX_map_eval₂ [CommSemiring R] [CommSemiring S] (f : R →+* S) (A : Matrix m n S) :
(mvPolynomialX m n R).map (MvPolynomial.eval₂ f fun p : m × n => A p.1 p.2) = A :=
ext fun i j => MvPolynomial.eval₂_X _ (fun p : m × n => A p.1 p.2) (i, j)
