mvPolynomialX_mapMatrix_aeval — Mathlib

English

A variant with a bundled AlgHom on the left: the aeval-map of mvPolynomialX yields A.

Русский

Вариант с объединенным AlgHom слева: aeval mvPolynomialX даёт A.

LaTeX

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

Lean4

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

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