mathlib
e6577119 - feat(analysis/normed_space/star/continuous_functional_calculus): prove spectral permanence and construct the `continuous_functional_calculus` (#17164)

Commit
2 years ago
feat(analysis/normed_space/star/continuous_functional_calculus): prove spectral permanence and construct the `continuous_functional_calculus` (#17164) This PR proves the **spectral permanence** property for C⋆-algebras and constructs the **continuous functional calculus** for normal elements. - [x] depends on: #17000 - [x] depends on: #17136 - [x] depends on: #17156 - [x] depends on: #17166 - [x] depends on: #17167 - [x] depends on: #17169 - [x] depends on: #17170 - [x] depends on: #17178 - [x] depends on: #17183 - [x] depends on: #17504
Author
Parents
Loading