Theorem mem_unitary_of_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 mem_unitary_of_spectrum_subset_unitary View on Github →