univ_coeff_eval₂Hom — Mathlib

English

For each i, the i-th coefficient of the eval₂Hom f applied to M equals the i-th coefficient of the characteristic polynomial of Matrix.of M.curry.

Русский

Для каждого индекса i i-й коэффициент eval₂Hom f(M) равен i-й коэффициенту характеристического полинома Matrix.of M.curry.

LaTeX

$$$\\operatorname{eval}_2 f M \\big((\\mathrm{univ }R\,n).\\operatorname{coeff} i\\big) = (\\mathrm{charpoly}(\\mathrm{Matrix.of} M.curry)).\\operatorname{coeff} i$$$

Lean4

@[simp]
theorem univ_coeff_eval₂Hom (M : n × n → S) (i : ℕ) :
    MvPolynomial.eval₂Hom f M ((univ R n).coeff i) = (charpoly (Matrix.of M.curry)).coeff i := by
  rw [← univ_map_eval₂Hom n f M, Polynomial.coeff_map]

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