OAI/Analysis/Commutator/FreeBlockTensor3.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FreeBlocks.factorOf line 32
2. def OAI.Kadison.FreeBlocks.letterOf line 35
3. lemma OAI.Kadison.FreeBlocks.factorValue_factorOf line 38
4. lemma OAI.Kadison.FreeBlocks.letterValue_letterOf line 41
5. lemma OAI.Kadison.FreeBlocks.tail_word_as_block line 45
6. lemma OAI.Kadison.FreeBlocks.word_as_endpoint line 75