polyCharpolyAux_map_eq_charpoly — Mathlib

English

For any x ∈ L and i ∈ Nat, the coefficient equality holds between polyCharpolyAux and the matrix-characteristic-polynomial coefficients.

Русский

Для любых x и i выполняется равенство коэффициентов между polyCharpolyAux и коэффициентами характеристического полинома матрицы.

LaTeX

$$MvPolynomial.coeff (polyCharpolyAux φ b b_m) i = polynomial_coefficient_corresponding_to_matrix(φ x) i$$

Lean4

@[simp]
theorem polyCharpolyAux_map_eq_charpoly [Module.Finite R M] [Module.Free R M] (x : L) :
    (polyCharpolyAux φ b bₘ).map (MvPolynomial.eval (b.repr x)) = (φ x).charpoly :=
  by
  nontriviality R
  rw [polyCharpolyAux_map_eq_toMatrix_charpoly, LinearMap.charpoly_toMatrix]

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