unitary_conjugate' — Mathlib

English

Let a ∈ A and u ∈ unitary A. Then spectrum((star u) a u) = spectrum(a).

Русский

Пусть a ∈ A и u ∈ unitary A. Тогда спектр((u^*) a u) равен спектру a.

LaTeX

$$$\mathrm{spec}_R\big((\star u) a u\big) = \mathrm{spec}_R(a)$$$

Lean4

/-- Unitary conjugation preserves the spectrum, star on right. -/
@[simp]
theorem unitary_conjugate' {a : A} {u : unitary A} : spectrum R ((star u : A) * a * u) = spectrum R a := by
  simpa using spectrum.unitary_conjugate (u := star u)

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