charpoly_units_conj'

Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

URI: https://scilib.ai/kg/mathlib#Matrix.charpoly_units_conj'

English

If M is a unit (invertible matrix) and N is any matrix, then charpoly(M^{-1} N M) = charpoly(N).

Русский

Если M — обратимая матрица, то charpoly(M^{-1} N M) = charpoly(N).

LaTeX

$$$$ \\operatorname{charpoly}(M^{-1} N M) = \\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 :=
  charpoly_units_conj M⁻¹ N

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru