OAI/Analysis/Commutator/FreeWordTensor.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Kadison.FreeWordTensor.FaithfulState line 23
  2. abbrev OAI.Kadison.FreeWordTensor.preSpace line 30
  3. instance OAI.Kadison.FreeWordTensor.faithfulNormed line 32
  4. def OAI.Kadison.FreeWordTensor.letterSpace line 43
  5. def OAI.Kadison.FreeWordTensor.letterValue line 51
  6. def OAI.Kadison.FreeWordTensor.asLetter line 54
  7. structure OAI.Kadison.FreeWordTensor.Space line 60
  8. instance OAI.Kadison.FreeWordTensor.(instance at line 67) line 67
  9. def OAI.Kadison.FreeWordTensor.tensor line 69
  10. def OAI.Kadison.FreeWordTensor.Params line 73
  11. def OAI.Kadison.FreeWordTensor.pure line 77
  12. def OAI.Kadison.FreeWordTensor.letters line 81
  13. lemma OAI.Kadison.FreeWordTensor.letters_colors line 85
  14. lemma OAI.Kadison.FreeWordTensor.letters_reduced line 90
  15. def OAI.Kadison.FreeWordTensor.read line 95
  16. lemma OAI.Kadison.FreeWordTensor.read_pure line 100
  17. lemma OAI.Kadison.FreeWordTensor.span_pure line 110
  18. lemma OAI.Kadison.FreeWordTensor.inner_letter line 138
  19. lemma OAI.Kadison.FreeWordTensor.inner_pure line 142
  20. def OAI.Kadison.FreeWordTensor.readPre line 151
  21. lemma OAI.Kadison.FreeWordTensor.readPre_pure line 154
  22. lemma OAI.Kadison.FreeWordTensor.inner_readPre_pure line 164
  23. lemma OAI.Kadison.FreeWordTensor.inner_readPre line 172
  24. def OAI.Kadison.FreeWordTensor.readIsometry line 191
  25. def OAI.Kadison.FreeWordTensor.wordEmbedding line 195
  26. lemma OAI.Kadison.FreeWordTensor.wordEmbedding_coe line 203
  27. lemma OAI.Kadison.FreeWordTensor.inner_readPre_pure_ne line 210
  28. lemma OAI.Kadison.FreeWordTensor.inner_readPre_ne line 222
  29. lemma OAI.Kadison.FreeWordTensor.wordEmbedding_orthogonal line 242
  30. def OAI.Kadison.FreeWordTensor.ColorSeq line 252
  31. abbrev OAI.Kadison.FreeWordTensor.wordSpace line 254
  32. def OAI.Kadison.FreeWordTensor.wordInclusion line 256
  33. lemma OAI.Kadison.FreeWordTensor.wordFamily_orthogonal line 259