Theorem spectrum_subset_unitary_of_mem_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 spectrum_subset_unitary_of_mem_unitary View on Github →