OAI/Analysis/Pureness/Quasitrace/QuasitraceFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CuntzPureness.ComplexQuasitrace line 10
2. instance OAI.CuntzPureness.(instance at line 18) line 18
3. def OAI.CuntzPureness.PositiveQuasitrace.toComplex line 23
4. structure OAI.CuntzPureness.CompatibleFiniteQuasitrace line 32
5. def OAI.CuntzPureness.finiteSpectralQuasitraceFamily line 36
6. lemma OAI.CuntzPureness.finiteSpectralQuasitraceFamily_positive line 50
7. theorem OAI.CuntzPureness.finiteSpectralQuasitraceFamily_root_rank line 57