trace_conjTranspose

Mathlib.LinearAlgebra.Matrix.Trace

URI: https://scilib.ai/kg/mathlib#Matrix.trace_conjTranspose

English

If the underlying ring has a star operation, tr(A^H) = star(tr(A)).

Русский

Если в базовом кольце есть операция сопряжения, то tr(A^H) = conj(tr(A)).

LaTeX

$$$$ \operatorname{tr}(A^{\mathsf{H}}) = \ast\big( \operatorname{tr}(A) \big) $$$$

Lean4

@[simp]
theorem trace_conjTranspose [StarAddMonoid R] (A : Matrix n n R) : trace Aᴴ = star (trace A) :=
  (star_sum _ _).symm

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

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

Разделы

Аффилиация

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