Theorems · Theorem · linear algebra

evalRingHom_mapMatrix_comp_polyToMatrix

∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {S : Type u_3}
  [inst_3 : CommSemiring S] (f : S →+* Matrix n n R),
  (Polynomial.evalRingHom 0).mapMatrix.comp f.polyToMatrix = f.comp (Polynomial.evalRingHom 0)

Defined in

Mathlib.RingTheory.MatrixPolynomialAlgebra

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringDecidableEqFintypeCommSemiring