charpoly_units_conj — Mathlib

English

If M is an invertible matrix and N is any matrix of the same size, then the characteristic polynomial is invariant under similarity: charpoly(M N M^{-1}) = charpoly(N).

Русский

Если M — обратимая матрица, а N — любая матрица той же размерности, то характеристический многочлен сохраняется при подобии: charpoly(M N M^{-1}) = charpoly(N).

LaTeX

$$$$ \\operatorname{charpoly}(M N M^{-1}) = \\operatorname{charpoly}(N). $$$$

Lean4

theorem charpoly_units_conj (M : (Matrix n n R)ˣ) (N : Matrix n n R) : (M.val * N * M⁻¹.val).charpoly = N.charpoly :=
  by
  rw [Matrix.charpoly_mul_comm, ← mul_assoc]
  simp

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