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]