OAI/Analysis/Pureness/Quasitrace/PositiveQuasitrace.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CuntzPureness.PositiveQuasitrace line 12
2. instance OAI.CuntzPureness.(instance at line 21) line 21
3. def OAI.CuntzPureness.finiteSpectralPositiveQuasitrace line 26
4. lemma OAI.CuntzPureness.finiteSpectralPositiveQuasitrace_inclusion line 43
5. lemma OAI.CuntzPureness.finiteSpectralPositiveQuasitrace_root_rank line 51