unitary_iff_isStarNormal_and_spectrum_subset_unitary

English

An element u is unitary iff it is star-normal and its spectrum lies in the unitary group; equivalently, membership in unitary is characterized by spectral properties.

Русский

Элемент u является единицей тогда и только тогда, когда он звездо-нормален и спектр лежит в группе единиц; эквивалентно, членство в unitary охарактеризуется спектральными свойствами.

LaTeX

$$u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ unitary ℂ$$

Lean4

theorem unitary_iff_isStarNormal_and_spectrum_subset_unitary {u : A} :
    u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ unitary ℂ :=
  by
  rw [← and_iff_right_of_imp isStarNormal_of_mem_unitary]
  refine and_congr_right fun hu ↦ ?_
  nth_rw 1 [← cfc_id ℂ u]
  rw [cfc_unitary_iff id u, Set.subset_def]
  simp only [id_eq, RCLike.star_def, SetLike.mem_coe, unitary.mem_iff_star_mul_self]

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