OAI/Analysis/Commutator/TracialVectorSubalgebra.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.VectorGNS.subalgebraTrace line 23
2. lemma OAI.Kadison.VectorGNS.subalgebraTrace_apply line 27
3. lemma OAI.Kadison.VectorGNS.subalgebraTrace_subtype line 30
4. lemma OAI.Kadison.VectorGNS.subalgebraTrace_normal line 33
5. abbrev OAI.Kadison.VectorGNS.subalgebraEmbedding line 38
6. abbrev OAI.Kadison.VectorGNS.subalgebraCompression line 42
7. lemma OAI.Kadison.VectorGNS.subalgebraEmbedding_coe line 47
8. lemma OAI.Kadison.VectorGNS.subalgebraCompression_on_preserved line 53
9. lemma OAI.Kadison.TracialSequence.subalgebra_tracial line 77
10. lemma OAI.Kadison.TracialSequence.subalgebra_faithful line 83
11. lemma OAI.Kadison.TracialSequence.subalgebra_normalized line 88
12. abbrev OAI.Kadison.TracialSequence.subalgebraState line 92