OAI/Analysis/Commutator/FreeActualStructure.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.FreeBlocks.embeddedSourceWord line 54
2. structure OAI.Kadison.FreeBlocks.WordActions line 62
3. def OAI.Kadison.FreeBlocks.tracialWordActions line 69
4. def OAI.Kadison.FreeBlocks.faithfulWordActions line 80
5. theorem OAI.Kadison.FreeBlocks.faithfulWordActions_eq line 92
6. abbrev OAI.Kadison.FreeBlocks.wordLevel line 98
7. abbrev OAI.Kadison.FreeBlocks.wordLeftAction line 103
8. abbrev OAI.Kadison.FreeBlocks.wordConjugationAction line 111
9. abbrev OAI.Kadison.FreeBlocks.wordStructure line 119
10. def OAI.Kadison.FreeBlocks.wordStructureRule line 141
11. theorem OAI.Kadison.FreeBlocks.tracial_word_structure line 166
12. theorem OAI.Kadison.FreeBlocks.faithful_word_structure line 183
13. lemma OAI.Kadison.FreeBlocks.faithful_left_level line 198
14. lemma OAI.Kadison.FreeBlocks.faithful_conjugation_level line 206
15. theorem OAI.Kadison.FreeBlocks.free_word_structure line 215