polyCharpoly_coeff_eval — Mathlib

English

For every x in L and every index i, the evaluation of the i-th coefficient of polyCharpoly φ b at x equals the i-th coefficient of the characteristic polynomial of φ x.

Русский

Для каждого x ∈ L и каждого индекса i равенства: оценка i-го коэффициента polyCharpoly φ b в точке x равна i-му коэффициенту характеристического полинома φ x.

LaTeX

$$$MvPolynomial.eval (b.repr x) ((\mathrm{polyCharpoly}\ φ\ b).\mathrm{coeff} i) = (φ x).\mathrm{charpoly}.\mathrm{coeff} i$$$

Lean4

@[simp]
theorem polyCharpoly_coeff_eval (x : L) (i : ℕ) :
    MvPolynomial.eval (b.repr x) ((polyCharpoly φ b).coeff i) = (φ x).charpoly.coeff i := by
  rw [polyCharpoly, polyCharpolyAux_coeff_eval]

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