OAI/Analysis/Commutator/FreeBlockWords.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.FreeCreation.inner_mul_two_wordVector line 33
2. lemma OAI.Kadison.FreeCreation.inner_mul_two_tailSpan line 46
3. lemma OAI.Kadison.FreeCreation.inner_mul_two_tailSpace line 65
4. lemma OAI.Kadison.FreeCreation.vacuum_mem_tailSpan line 81
5. lemma OAI.Kadison.FreeCreation.factor_vector_mem_tailSpan line 84
6. lemma OAI.Kadison.FreeCreation.factor_vector_mem_tailSpace line 98