univ_map_eval₂Hom — Mathlib

English

For a ring hom f: R →+* S and a matrix M : n × n → S, applying eval₂Hom f to M on the universal polynomial matches the characteristic polynomial of Matrix.of M.curry.

Русский

Для кольцевого гомоморфа f: R →+* S и матрицы M : n × n → S применение eval₂Hom f к M в рамках универсального многочлена даёт характеристический полином Matrix.of M.curry.

LaTeX

$$$(\\mathrm{univ}\,R\,n).map (\\mathrm{eval}_{2\\!} f M) = \\mathrm{charpoly}(\\mathrm{Matrix.of} (M.curry))$$$

Lean4

@[simp]
theorem univ_map_eval₂Hom (M : n × n → S) : (univ R n).map (eval₂Hom f M) = charpoly (Matrix.of M.curry) :=
  by
  rw [univ, ← charpoly_map, coe_eval₂Hom, ← mvPolynomialX_map_eval₂ f (Matrix.of M.curry)]
  simp only [of_apply, Function.curry_apply, Prod.mk.eta]

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