OAI/Analysis/Commutator/VonNeumannCStar.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Kadison.VonNeumannCStar.isClosed line 15
2. instance OAI.Kadison.VonNeumannCStar.smulMemClass line 20
3. instance OAI.Kadison.VonNeumannCStar.cstarAlgebra line 23
4. lemma OAI.Kadison.VonNeumannCStar.sqrt_mem line 26
5. instance OAI.Kadison.VonNeumannCStar.starOrderedRing line 32