mvPolynomialX_mapMatrix_eval — Mathlib

English

A variant of mvPolynomialX_map_eval₂ with a bundled RingHom on the left: evaluating and mapping yields the original matrix A.

Русский

Вариант mvPolynomialX_map_eval₂ с упаковкой кольцевого однозначного отображения слева: при отображении получаем исходную матрицу A.

LaTeX

$$$(MvPolynomial.eval\ fun p => A_{p.1 p.2}).mapMatrix (mvPolynomialX_{m m,R}) = A$$$

Lean4

/-- A variant of `Matrix.mvPolynomialX_map_eval₂` with a bundled `RingHom` on the LHS. -/
theorem mvPolynomialX_mapMatrix_eval [Fintype m] [DecidableEq m] [CommSemiring R] (A : Matrix m m R) :
    (MvPolynomial.eval fun p : m × m => A p.1 p.2).mapMatrix (mvPolynomialX m m R) = A :=
  mvPolynomialX_map_eval₂ _ A

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