OAI/Analysis/Commutator/FreeBlockTensor2.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.FreeBlocks.blockReadPre_mem_tail line 33
  2. lemma OAI.Kadison.FreeBlocks.inner_blockReadPre_ne line 48
  3. def OAI.Kadison.FreeBlocks.endpointTensor line 70
  4. def OAI.Kadison.FreeBlocks.endpointRead line 73
  5. lemma OAI.Kadison.FreeBlocks.endpointRead_tmul line 78
  6. lemma OAI.Kadison.FreeBlocks.endpointTensor_induction_on line 86
  7. lemma OAI.Kadison.FreeBlocks.inner_endpointRead_tmul line 95
  8. lemma OAI.Kadison.FreeBlocks.inner_endpointRead line 108
  9. lemma OAI.Kadison.FreeBlocks.inner_endpointRead_ne line 127
  10. def OAI.Kadison.FreeBlocks.endpointIsometry line 144
  11. def OAI.Kadison.FreeBlocks.levelEmbedding line 147
  12. lemma OAI.Kadison.FreeBlocks.levelEmbedding_coe line 154
  13. lemma OAI.Kadison.FreeBlocks.levelEmbedding_orthogonal line 160
  14. lemma OAI.Kadison.FreeBlocks.levelFamily_orthogonal line 169