OAI/Analysis/Commutator/AbelianGNSSpectral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Kadison.CentralSpectral.centerCommCStar line 23
2. abbrev OAI.Kadison.CentralSpectral.Spectrum line 27
3. instance OAI.Kadison.CentralSpectral.spectrumMeasurable line 29
4. instance OAI.Kadison.CentralSpectral.spectrumBorel line 31
5. theorem OAI.Kadison.CentralSpectral.exists_center_gns_model line 33