OAI/Analysis/Commutator/Regroup.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.FreeBlocks.dLetters line 37
  2. def OAI.Kadison.FreeBlocks.aLetters line 39
  3. def OAI.Kadison.FreeBlocks.multiplicityTensor line 41
  4. def OAI.Kadison.FreeBlocks.paramD line 45
  5. def OAI.Kadison.FreeBlocks.paramJ line 49
  6. def OAI.Kadison.FreeBlocks.blockShuffle line 53
  7. lemma OAI.Kadison.FreeBlocks.blockShuffle_pure line 64
  8. def OAI.Kadison.FreeBlocks.endpointShuffle line 83
  9. lemma OAI.Kadison.FreeBlocks.endpointShuffle_pure line 90
  10. abbrev OAI.Kadison.FreeBlocks.scalarLevel line 99
  11. abbrev OAI.Kadison.FreeBlocks.multiplicityLevel line 102
  12. def OAI.Kadison.FreeBlocks.levelShuffle line 104
  13. lemma OAI.Kadison.FreeBlocks.levelShuffle_pure line 108