trace_units_conj'

Mathlib.LinearAlgebra.Matrix.Trace

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

← MathLib Explorer

English

For an invertible matrix M and any N, tr(M^{-1} N M) = tr(N).

Русский

Для обратимой матрицы M и любой N выполняется tr(M^{-1} N M) = tr(N).

LaTeX

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

Lean4

theorem trace_units_conj' (M : (Matrix m m R)ˣ) (N : Matrix m m R) :
    trace ((↑M⁻¹ : Matrix _ _ _) * N * (↑M : Matrix _ _ _)) = trace N :=
  trace_units_conj M⁻¹ N

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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