OAI/Analysis/Commutator/TracialSequenceRight.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.TracialSequence.vectorIn line 24
2. lemma OAI.Kadison.TracialSequence.vectorIn_coe line 26
3. lemma OAI.Kadison.TracialSequence.leftRestricted_vector line 28
4. lemma OAI.Kadison.TracialSequence.operator_ext line 33
5. def OAI.Kadison.TracialSequence.sequenceVacuum line 50
6. lemma OAI.Kadison.TracialSequence.leftRestricted_vacuum line 52
7. def OAI.Kadison.TracialSequence.rightFamily line 58
8. lemma OAI.Kadison.TracialSequence.rightFamily_apply line 65
9. def OAI.Kadison.TracialSequence.rightAction line 68
10. lemma OAI.Kadison.TracialSequence.rightAction_vector line 71
11. lemma OAI.Kadison.TracialSequence.rightAction_preserves line 84
12. def OAI.Kadison.TracialSequence.rightRestricted line 94
13. lemma OAI.Kadison.TracialSequence.rightRestricted_vector line 97
14. lemma OAI.Kadison.TracialSequence.rightRestricted_vacuum line 102
15. lemma OAI.Kadison.TracialSequence.left_right line 106
16. lemma OAI.Kadison.TracialSequence.right_mem_commutant line 113
17. lemma OAI.Kadison.TracialSequence.bicommutant_eq_of_vacuum line 119