OAI/Analysis/JiangSu/CuntzSemigroup/QuasitraceFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Pureness.ComplexQuasitrace line 14
2. instance OAI.Pureness.(instance at line 22) line 22
3. def OAI.Pureness.PositiveQuasitrace.toComplex line 27
4. structure OAI.Pureness.CompatibleFiniteQuasitrace line 36
5. def OAI.Pureness.finiteSpectralQuasitraceFamily line 40
6. lemma OAI.Pureness.finiteSpectralQuasitraceFamily_positive line 54
7. theorem OAI.Pureness.finiteSpectralQuasitraceFamily_root_rank line 61