OAI/Analysis/Pureness/Quasitrace/CentralQuasitraceCompression.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.ComplexQuasitrace.map_add_commuting_selfAdjoint line 11
2. def OAI.CuntzPureness.centralProjectionHom line 44
3. def OAI.CuntzPureness.ComplexQuasitrace.centralCompression line 60
4. lemma OAI.CuntzPureness.ComplexQuasitrace.centralCompression_apply line 64
5. theorem OAI.CuntzPureness.ComplexQuasitrace.central_projection_split line 68