OAI/Analysis/MutuallyUnbiased/GramAssembly/Block5Part4.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block5.node128 line 8
  2. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node128_check line 10
  3. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node128_eval line 13
  4. def OAI.MUB6.Certificate.GramAssembly.Block5.node129 line 18
  5. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node129_check line 20
  6. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node129_eval line 23
  7. def OAI.MUB6.Certificate.GramAssembly.Block5.node130 line 29
  8. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node130_check line 31
  9. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node130_eval line 34
  10. def OAI.MUB6.Certificate.GramAssembly.Block5.node131 line 39
  11. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node131_check line 41
  12. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node131_eval line 44
  13. def OAI.MUB6.Certificate.GramAssembly.Block5.node132 line 49
  14. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node132_check line 51
  15. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node132_eval line 54
  16. def OAI.MUB6.Certificate.GramAssembly.Block5.node133 line 58
  17. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node133_check line 60
  18. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node133_eval line 63
  19. def OAI.MUB6.Certificate.GramAssembly.Block5.node134 line 68
  20. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node134_check line 70
  21. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node134_eval line 73
  22. def OAI.MUB6.Certificate.GramAssembly.Block5.node135 line 77
  23. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node135_check line 79
  24. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node135_eval line 82
  25. def OAI.MUB6.Certificate.GramAssembly.Block5.node136part0 line 87
  26. def OAI.MUB6.Certificate.GramAssembly.Block5.node136part1 line 89
  27. def OAI.MUB6.Certificate.GramAssembly.Block5.node136part2 line 91
  28. def OAI.MUB6.Certificate.GramAssembly.Block5.node136part3 line 93
  29. def OAI.MUB6.Certificate.GramAssembly.Block5.node136part4 line 95
  30. def OAI.MUB6.Certificate.GramAssembly.Block5.node136part5 line 97
  31. def OAI.MUB6.Certificate.GramAssembly.Block5.node136part6 line 99
  32. def OAI.MUB6.Certificate.GramAssembly.Block5.node136part7 line 101
  33. def OAI.MUB6.Certificate.GramAssembly.Block5.node136 line 103
  34. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node136_check line 105
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node136_eval line 108
  36. def OAI.MUB6.Certificate.GramAssembly.Block5.node137 line 113
  37. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node137_check line 115
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node137_eval line 118
  39. def OAI.MUB6.Certificate.GramAssembly.Block5.node138 line 122
  40. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node138_check line 124
  41. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node138_eval line 127
  42. def OAI.MUB6.Certificate.GramAssembly.Block5.node139 line 132
  43. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node139_check line 134
  44. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node139_eval line 137
  45. def OAI.MUB6.Certificate.GramAssembly.Block5.node140 line 141
  46. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node140_check line 143
  47. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node140_eval line 146
  48. def OAI.MUB6.Certificate.GramAssembly.Block5.node141part0 line 151
  49. def OAI.MUB6.Certificate.GramAssembly.Block5.node141part1 line 153
  50. def OAI.MUB6.Certificate.GramAssembly.Block5.node141part2 line 155
  51. def OAI.MUB6.Certificate.GramAssembly.Block5.node141part3 line 157
  52. def OAI.MUB6.Certificate.GramAssembly.Block5.node141part4 line 159
  53. def OAI.MUB6.Certificate.GramAssembly.Block5.node141part5 line 161
  54. def OAI.MUB6.Certificate.GramAssembly.Block5.node141part6 line 163
  55. def OAI.MUB6.Certificate.GramAssembly.Block5.node141 line 165
  56. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node141_check line 167
  57. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node141_eval line 170
  58. def OAI.MUB6.Certificate.GramAssembly.Block5.node142part0 line 175
  59. def OAI.MUB6.Certificate.GramAssembly.Block5.node142part1 line 177
  60. def OAI.MUB6.Certificate.GramAssembly.Block5.node142part2 line 179
  61. def OAI.MUB6.Certificate.GramAssembly.Block5.node142part3 line 181
  62. def OAI.MUB6.Certificate.GramAssembly.Block5.node142part4 line 183
  63. def OAI.MUB6.Certificate.GramAssembly.Block5.node142part5 line 185
  64. def OAI.MUB6.Certificate.GramAssembly.Block5.node142part6 line 187
  65. def OAI.MUB6.Certificate.GramAssembly.Block5.node142part7 line 189
  66. def OAI.MUB6.Certificate.GramAssembly.Block5.node142part8 line 191
  67. def OAI.MUB6.Certificate.GramAssembly.Block5.node142part9 line 193
  68. def OAI.MUB6.Certificate.GramAssembly.Block5.node142 line 195
  69. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node142_check line 197
  70. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node142_eval line 200