OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part9.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block4.node288 line 8
  2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node288_check line 10
  3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node288_eval line 13
  4. def OAI.MUB6.Certificate.GramAssembly.Block4.node289 line 19
  5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node289_check line 21
  6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node289_eval line 24
  7. def OAI.MUB6.Certificate.GramAssembly.Block4.node290 line 29
  8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node290_check line 31
  9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node290_eval line 34
  10. def OAI.MUB6.Certificate.GramAssembly.Block4.node291 line 40
  11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node291_check line 42
  12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node291_eval line 45
  13. def OAI.MUB6.Certificate.GramAssembly.Block4.node292 line 50
  14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node292_check line 52
  15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node292_eval line 55
  16. def OAI.MUB6.Certificate.GramAssembly.Block4.node293 line 60
  17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node293_check line 62
  18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node293_eval line 65
  19. def OAI.MUB6.Certificate.GramAssembly.Block4.node294 line 70
  20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node294_check line 72
  21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node294_eval line 75
  22. def OAI.MUB6.Certificate.GramAssembly.Block4.node295 line 80
  23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node295_check line 82
  24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node295_eval line 85
  25. def OAI.MUB6.Certificate.GramAssembly.Block4.node296 line 90
  26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node296_check line 92
  27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node296_eval line 95
  28. def OAI.MUB6.Certificate.GramAssembly.Block4.node297 line 101
  29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node297_check line 103
  30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node297_eval line 106
  31. def OAI.MUB6.Certificate.GramAssembly.Block4.node298 line 111
  32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node298_check line 113
  33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node298_eval line 116
  34. def OAI.MUB6.Certificate.GramAssembly.Block4.node299 line 121
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node299_check line 123
  36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node299_eval line 126
  37. def OAI.MUB6.Certificate.GramAssembly.Block4.node300 line 132
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node300_check line 134
  39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node300_eval line 137
  40. def OAI.MUB6.Certificate.GramAssembly.Block4.node301 line 142
  41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node301_check line 144
  42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node301_eval line 147
  43. def OAI.MUB6.Certificate.GramAssembly.Block4.node302 line 153
  44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node302_check line 155
  45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node302_eval line 158
  46. def OAI.MUB6.Certificate.GramAssembly.Block4.node303 line 163
  47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node303_check line 165
  48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node303_eval line 168
  49. def OAI.MUB6.Certificate.GramAssembly.Block4.node304 line 173
  50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node304_check line 175
  51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node304_eval line 178
  52. def OAI.MUB6.Certificate.GramAssembly.Block4.node305 line 183
  53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node305_check line 185
  54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node305_eval line 188
  55. def OAI.MUB6.Certificate.GramAssembly.Block4.node306 line 193
  56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node306_check line 195
  57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node306_eval line 198
  58. def OAI.MUB6.Certificate.GramAssembly.Block4.node307 line 204
  59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node307_check line 206
  60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node307_eval line 209
  61. def OAI.MUB6.Certificate.GramAssembly.Block4.node308 line 214
  62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node308_check line 216
  63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node308_eval line 219
  64. def OAI.MUB6.Certificate.GramAssembly.Block4.node309 line 224
  65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node309_check line 226
  66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node309_eval line 229
  67. def OAI.MUB6.Certificate.GramAssembly.Block4.node310 line 235
  68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node310_check line 237
  69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node310_eval line 240
  70. def OAI.MUB6.Certificate.GramAssembly.Block4.node311 line 245
  71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node311_check line 247
  72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node311_eval line 250
  73. def OAI.MUB6.Certificate.GramAssembly.Block4.node312 line 256
  74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node312_check line 258
  75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node312_eval line 261
  76. def OAI.MUB6.Certificate.GramAssembly.Block4.node313 line 266
  77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node313_check line 268
  78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node313_eval line 271
  79. def OAI.MUB6.Certificate.GramAssembly.Block4.node314 line 276
  80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node314_check line 278
  81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node314_eval line 281
  82. def OAI.MUB6.Certificate.GramAssembly.Block4.node315 line 286
  83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node315_check line 288
  84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node315_eval line 291
  85. def OAI.MUB6.Certificate.GramAssembly.Block4.node316 line 296
  86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node316_check line 298
  87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node316_eval line 301
  88. def OAI.MUB6.Certificate.GramAssembly.Block4.node317 line 306
  89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node317_check line 308
  90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node317_eval line 311
  91. def OAI.MUB6.Certificate.GramAssembly.Block4.node318 line 317
  92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node318_check line 319
  93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node318_eval line 322
  94. def OAI.MUB6.Certificate.GramAssembly.Block4.node319 line 327
  95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node319_check line 329
  96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node319_eval line 332