Theorems · Theorem · linear algebra

Matrix.mvPolynomialX_mapMatrix_aeval

∀ {m : Type u_1} (R : Type u_3) {S : Type u_4} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
  [inst_3 : CommSemiring S] [inst_4 : Algebra R S] (A : Matrix m m S),
  (MvPolynomial.aeval fun p => A p.1 p.2).mapMatrix (Matrix.mvPolynomialX m m R) = A

A variant of Matrix.mvPolynomialX_map_eval₂ with a bundled AlgHom on the LHS.

Defined in

Mathlib.LinearAlgebra.Matrix.MvPolynomial

Cited by

2 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqCommSemiringCommSemiringAlgebra