polyCharpolyAux_coeff_eval — Mathlib

English

For any x, the map of polyCharpolyAux by eval gives the same as the charpoly of φ x.

Русский

При отображении через eval полином polyCharpolyAux совпадает с характеристическим полиномом φ x.

LaTeX

$$(polyCharpolyAux φ b b_m).map (MvPolynomial.eval (b.repr x)) = (φ x).charpoly$$

Lean4

@[simp]
theorem polyCharpolyAux_coeff_eval [Module.Finite R M] [Module.Free R M] (x : L) (i : ℕ) :
    MvPolynomial.eval (b.repr x) ((polyCharpolyAux φ b bₘ).coeff i) = (φ x).charpoly.coeff i :=
  by
  nontriviality R
  rw [← polyCharpolyAux_map_eq_charpoly φ b bₘ x, Polynomial.coeff_map]

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