polyCharpolyAux_map_eq_toMatrix_charpoly

English

For any x, the evaluated polyCharpolyAux at x equals the characteristic polynomial of φ x.

Русский

При подстановке x характеристический полином φ x равен результату сопоставления polyCharpolyAux.

LaTeX

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

Lean4

theorem polyCharpolyAux_map_eq_toMatrix_charpoly (x : L) :
    (polyCharpolyAux φ b bₘ).map (MvPolynomial.eval (b.repr x)) = (toMatrix bₘ bₘ (φ x)).charpoly :=
  by
  rw [polyCharpolyAux, Polynomial.map_map, ← MvPolynomial.eval₂Hom_C_eq_bind₁, MvPolynomial.comp_eval₂Hom,
    charpoly.univ_map_eval₂Hom]
  congr
  ext
  rw [of_apply, Function.curry_apply, toMvPolynomial_eval_eq_apply, LinearEquiv.symm_apply_apply]
  rfl

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