unitary_conjugate — Mathlib

English

For a, u in a C*-algebra with unitary u, spectrum is preserved under conjugation: spectrum(u a u^*) = spectrum(a).

Русский

Для нормального элемента a и унитарного u спектр сохраняется при сопряжении: спектр(u a u^*) = спектр(a).

LaTeX

$$$\mathrm{spec}_R(u a u^{*}) = \mathrm{spec}_R(a)$$$

Lean4

/-- Unitary conjugation preserves the spectrum, star on left. -/
@[simp]
theorem unitary_conjugate {a : A} {u : unitary A} : spectrum R (u * a * (star u : A)) = spectrum R a :=
  spectrum.units_conjugate (u := unitary.toUnits u)

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