mem_unitary_of_spectrum_subset_unitary

English

If the spectrum of u is contained in the unitary group, then u is unitary.

Русский

Если спектр элемента u подмножество группы единиц, то u сам является единицей.

LaTeX

$$u ∈ unitary A$$

Lean4

theorem mem_unitary_of_spectrum_subset_unitary {u : A} [IsStarNormal u] (hu : spectrum ℂ u ⊆ unitary ℂ) :
    u ∈ unitary A :=
  unitary_iff_isStarNormal_and_spectrum_subset_unitary.mpr ⟨‹_›, hu⟩

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