OAI/Analysis/Commutator/FreeBlockTensor.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.FreeBlocks.factorSpace line 32
  2. def OAI.Kadison.FreeBlocks.factorValue line 38
  3. abbrev OAI.Kadison.FreeBlocks.spaceTensor line 41
  4. def OAI.Kadison.FreeBlocks.blockTensor line 43
  5. def OAI.Kadison.FreeBlocks.BlockParams line 47
  6. def OAI.Kadison.FreeBlocks.blockPure line 51
  7. def OAI.Kadison.FreeBlocks.paramLetters line 55
  8. def OAI.Kadison.FreeBlocks.paramEnd line 59
  9. lemma OAI.Kadison.FreeBlocks.paramLetters_length line 63
  10. def OAI.Kadison.FreeBlocks.blockRead line 68
  11. lemma OAI.Kadison.FreeBlocks.blockRead_pure line 75
  12. lemma OAI.Kadison.FreeBlocks.span_blockPure line 85
  13. def OAI.Kadison.FreeBlocks.blockReadPre line 110
  14. lemma OAI.Kadison.FreeBlocks.blockReadPre_pure line 113
  15. lemma OAI.Kadison.FreeBlocks.inner_blockReadPre_pure line 124
  16. lemma OAI.Kadison.FreeBlocks.inner_blockReadPre line 146
  17. def OAI.Kadison.FreeBlocks.blockIsometry line 162
  18. def OAI.Kadison.FreeBlocks.blockEmbedding line 165