evalRingHom_mapMatrix_comp_polyToMatrix

English

Evaluation at 0 composed with polyToMatrix equals the original evaluation map after composing with evalRingHom 0 on matrices.

Русский

Оценка при 0 после polyToMatrix равна исходной оценке после композиции с evalRingHom 0 на матрицах.

LaTeX

$$$(\\mathrm{evalRingHom}\\;0).\\mathrm{mapMatrix} \\circ f.polyToMatrix = f \\circ (\\mathrm{evalRingHom}\\;0) $$$

Lean4

theorem evalRingHom_mapMatrix_comp_polyToMatrix :
    (evalRingHom 0).mapMatrix.comp f.polyToMatrix = f.comp (evalRingHom 0) := by
  ext <;> simp [RingHom.polyToMatrix, -AlgEquiv.symm_toRingEquiv, diagonal, apply_ite]

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