charpoly_map — Mathlib

English

The charpoly of a mapped matrix equals the mapped charpoly of the original matrix: (M.map f).charpoly = M.charpoly.map f.

Русский

Характеристический многочлен матрицы после отображения равен отображённому характеристическому многочлену исходной матрицы: (M.map f).charpoly = M.charpoly.map f.

LaTeX

$$$\operatorname{charpoly}(M.map f) = (\operatorname{charpoly}(M)).map f$$$

Lean4

theorem charpoly_map (M : Matrix n n R) (f : R →+* S) : (M.map f).charpoly = M.charpoly.map f := by
  rw [charpoly, charmatrix_map, ← Polynomial.coe_mapRingHom, charpoly, RingHom.map_det, RingHom.mapMatrix_apply]

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