OAI/Analysis/Commutator/FreeSymmetry6.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.TracialGNS.wordLeft_inner line 28
2. lemma OAI.Kadison.TracialGNS.wordLeft_word line 36
3. lemma OAI.Kadison.TracialGNS.word_inner_move_endpoint line 49
4. lemma OAI.Kadison.TracialGNS.word_inner_stageCoefficient line 73
5. lemma OAI.Kadison.TracialGNS.centeredStageVector_of_trace_zero line 94
6. lemma OAI.Kadison.TracialGNS.centeredStageVector_inner line 100
7. theorem OAI.Kadison.TracialGNS.stageWord_inner_classification line 111