polyCharpoly_map_eq_charpoly — Mathlib

English

For any x in L, evaluating the coefficient-wise polynomial (polyCharpoly φ b) at x via the basis-representation b.repr x yields the characteristic polynomial of φ x.

Русский

Пусть x ∈ L; применение полинома polyCharpoly φ b к представлению b.repr x по основанию даёт характеристический полином отображения φ x.

LaTeX

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

Lean4

@[simp]
theorem polyCharpoly_map_eq_charpoly (x : L) : (polyCharpoly φ b).map (MvPolynomial.eval (b.repr x)) = (φ x).charpoly :=
  by rw [polyCharpoly, polyCharpolyAux_map_eq_charpoly]

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