polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff

English

For x in L and i in N, the evaluation coefficient matches the coefficient of the matrix characteristic polynomial of φ x at i.

Русский

Для x в L и i в N коэффициент при X^i в полиномe φ x совпадает с коэффициентом характеристического полинома матрицы φ x.

LaTeX

$$MvPolynomial.eval (b.repr x) ((polyCharpolyAux φ b b_m).coeff i) = (toMatrix b_m b_m (φ x)).charpoly.coeff i$$

Lean4

theorem polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff (x : L) (i : ℕ) :
    MvPolynomial.eval (b.repr x) ((polyCharpolyAux φ b bₘ).coeff i) = (toMatrix bₘ bₘ (φ x)).charpoly.coeff i := by
  simp [← polyCharpolyAux_map_eq_toMatrix_charpoly φ b bₘ x]

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