Theorem unitary_iff_isStarNormal_and_spectrum_subset_unitary

Modification history

2024-08-01 04:08

Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/Unitary.lean

refactor: remove some dependence on `circle` in C⋆-algebras (#15343)

Added unitary_iff_isStarNormal_and_spectrum_subset_unitary View on Github →