OAI/Analysis/MutuallyUnbiased/GramData/Block2.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

Exact integer matrix for λ = (1, 2, 2), m = 11, exponent = 13.

  1. def OAI.MUB6.Certificate.GramData.Block2.Z line 14
  2. def OAI.MUB6.Certificate.GramData.Block2.entries line 28
  3. def OAI.MUB6.Certificate.GramData.Block2.D line 42
  4. theorem OAI.MUB6.Certificate.GramData.Block2.pivot_0 line 44
  5. theorem OAI.MUB6.Certificate.GramData.Block2.pivot_1 line 46
  6. theorem OAI.MUB6.Certificate.GramData.Block2.pivot_2 line 48
  7. theorem OAI.MUB6.Certificate.GramData.Block2.pivot_3 line 50
  8. theorem OAI.MUB6.Certificate.GramData.Block2.pivot_4 line 52
  9. theorem OAI.MUB6.Certificate.GramData.Block2.pivot_5 line 54
  10. theorem OAI.MUB6.Certificate.GramData.Block2.pivot_6 line 56
  11. theorem OAI.MUB6.Certificate.GramData.Block2.pivot_7 line 58
  12. theorem OAI.MUB6.Certificate.GramData.Block2.pivot_8 line 60
  13. theorem OAI.MUB6.Certificate.GramData.Block2.pivot_9 line 62
  14. theorem OAI.MUB6.Certificate.GramData.Block2.pivot_10 line 64
  15. theorem OAI.MUB6.Certificate.GramData.Block2.entry_0_0 line 66
  16. theorem OAI.MUB6.Certificate.GramData.Block2.entry_0_1 line 70
  17. theorem OAI.MUB6.Certificate.GramData.Block2.entry_0_2 line 74
  18. theorem OAI.MUB6.Certificate.GramData.Block2.entry_0_3 line 78
  19. theorem OAI.MUB6.Certificate.GramData.Block2.entry_0_4 line 82
  20. theorem OAI.MUB6.Certificate.GramData.Block2.entry_0_5 line 86
  21. theorem OAI.MUB6.Certificate.GramData.Block2.entry_0_6 line 90
  22. theorem OAI.MUB6.Certificate.GramData.Block2.entry_0_7 line 94
  23. theorem OAI.MUB6.Certificate.GramData.Block2.entry_0_8 line 98
  24. theorem OAI.MUB6.Certificate.GramData.Block2.entry_0_9 line 102
  25. theorem OAI.MUB6.Certificate.GramData.Block2.entry_0_10 line 106
  26. theorem OAI.MUB6.Certificate.GramData.Block2.entry_1_0 line 110
  27. theorem OAI.MUB6.Certificate.GramData.Block2.entry_1_1 line 114
  28. theorem OAI.MUB6.Certificate.GramData.Block2.entry_1_2 line 118
  29. theorem OAI.MUB6.Certificate.GramData.Block2.entry_1_3 line 122
  30. theorem OAI.MUB6.Certificate.GramData.Block2.entry_1_4 line 126
  31. theorem OAI.MUB6.Certificate.GramData.Block2.entry_1_5 line 130
  32. theorem OAI.MUB6.Certificate.GramData.Block2.entry_1_6 line 134
  33. theorem OAI.MUB6.Certificate.GramData.Block2.entry_1_7 line 138
  34. theorem OAI.MUB6.Certificate.GramData.Block2.entry_1_8 line 142
  35. theorem OAI.MUB6.Certificate.GramData.Block2.entry_1_9 line 146
  36. theorem OAI.MUB6.Certificate.GramData.Block2.entry_1_10 line 150
  37. theorem OAI.MUB6.Certificate.GramData.Block2.entry_2_0 line 154
  38. theorem OAI.MUB6.Certificate.GramData.Block2.entry_2_1 line 158
  39. theorem OAI.MUB6.Certificate.GramData.Block2.entry_2_2 line 162
  40. theorem OAI.MUB6.Certificate.GramData.Block2.entry_2_3 line 166
  41. theorem OAI.MUB6.Certificate.GramData.Block2.entry_2_4 line 170
  42. theorem OAI.MUB6.Certificate.GramData.Block2.entry_2_5 line 174
  43. theorem OAI.MUB6.Certificate.GramData.Block2.entry_2_6 line 178
  44. theorem OAI.MUB6.Certificate.GramData.Block2.entry_2_7 line 182
  45. theorem OAI.MUB6.Certificate.GramData.Block2.entry_2_8 line 186
  46. theorem OAI.MUB6.Certificate.GramData.Block2.entry_2_9 line 190
  47. theorem OAI.MUB6.Certificate.GramData.Block2.entry_2_10 line 194
  48. theorem OAI.MUB6.Certificate.GramData.Block2.entry_3_0 line 198
  49. theorem OAI.MUB6.Certificate.GramData.Block2.entry_3_1 line 202
  50. theorem OAI.MUB6.Certificate.GramData.Block2.entry_3_2 line 206
  51. theorem OAI.MUB6.Certificate.GramData.Block2.entry_3_3 line 210
  52. theorem OAI.MUB6.Certificate.GramData.Block2.entry_3_4 line 214
  53. theorem OAI.MUB6.Certificate.GramData.Block2.entry_3_5 line 218
  54. theorem OAI.MUB6.Certificate.GramData.Block2.entry_3_6 line 222
  55. theorem OAI.MUB6.Certificate.GramData.Block2.entry_3_7 line 226
  56. theorem OAI.MUB6.Certificate.GramData.Block2.entry_3_8 line 230
  57. theorem OAI.MUB6.Certificate.GramData.Block2.entry_3_9 line 234
  58. theorem OAI.MUB6.Certificate.GramData.Block2.entry_3_10 line 238
  59. theorem OAI.MUB6.Certificate.GramData.Block2.entry_4_0 line 242
  60. theorem OAI.MUB6.Certificate.GramData.Block2.entry_4_1 line 246
  61. theorem OAI.MUB6.Certificate.GramData.Block2.entry_4_2 line 250
  62. theorem OAI.MUB6.Certificate.GramData.Block2.entry_4_3 line 254
  63. theorem OAI.MUB6.Certificate.GramData.Block2.entry_4_4 line 258
  64. theorem OAI.MUB6.Certificate.GramData.Block2.entry_4_5 line 262
  65. theorem OAI.MUB6.Certificate.GramData.Block2.entry_4_6 line 266
  66. theorem OAI.MUB6.Certificate.GramData.Block2.entry_4_7 line 270
  67. theorem OAI.MUB6.Certificate.GramData.Block2.entry_4_8 line 274
  68. theorem OAI.MUB6.Certificate.GramData.Block2.entry_4_9 line 278
  69. theorem OAI.MUB6.Certificate.GramData.Block2.entry_4_10 line 282
  70. theorem OAI.MUB6.Certificate.GramData.Block2.entry_5_0 line 286
  71. theorem OAI.MUB6.Certificate.GramData.Block2.entry_5_1 line 290
  72. theorem OAI.MUB6.Certificate.GramData.Block2.entry_5_2 line 294
  73. theorem OAI.MUB6.Certificate.GramData.Block2.entry_5_3 line 298
  74. theorem OAI.MUB6.Certificate.GramData.Block2.entry_5_4 line 302
  75. theorem OAI.MUB6.Certificate.GramData.Block2.entry_5_5 line 306
  76. theorem OAI.MUB6.Certificate.GramData.Block2.entry_5_6 line 310
  77. theorem OAI.MUB6.Certificate.GramData.Block2.entry_5_7 line 314
  78. theorem OAI.MUB6.Certificate.GramData.Block2.entry_5_8 line 318
  79. theorem OAI.MUB6.Certificate.GramData.Block2.entry_5_9 line 322
  80. theorem OAI.MUB6.Certificate.GramData.Block2.entry_5_10 line 326
  81. theorem OAI.MUB6.Certificate.GramData.Block2.entry_6_0 line 330
  82. theorem OAI.MUB6.Certificate.GramData.Block2.entry_6_1 line 334
  83. theorem OAI.MUB6.Certificate.GramData.Block2.entry_6_2 line 338
  84. theorem OAI.MUB6.Certificate.GramData.Block2.entry_6_3 line 342
  85. theorem OAI.MUB6.Certificate.GramData.Block2.entry_6_4 line 346
  86. theorem OAI.MUB6.Certificate.GramData.Block2.entry_6_5 line 350
  87. theorem OAI.MUB6.Certificate.GramData.Block2.entry_6_6 line 354
  88. theorem OAI.MUB6.Certificate.GramData.Block2.entry_6_7 line 358
  89. theorem OAI.MUB6.Certificate.GramData.Block2.entry_6_8 line 362
  90. theorem OAI.MUB6.Certificate.GramData.Block2.entry_6_9 line 366
  91. theorem OAI.MUB6.Certificate.GramData.Block2.entry_6_10 line 370
  92. theorem OAI.MUB6.Certificate.GramData.Block2.entry_7_0 line 374
  93. theorem OAI.MUB6.Certificate.GramData.Block2.entry_7_1 line 378
  94. theorem OAI.MUB6.Certificate.GramData.Block2.entry_7_2 line 382
  95. theorem OAI.MUB6.Certificate.GramData.Block2.entry_7_3 line 386
  96. theorem OAI.MUB6.Certificate.GramData.Block2.entry_7_4 line 390
  97. theorem OAI.MUB6.Certificate.GramData.Block2.entry_7_5 line 394
  98. theorem OAI.MUB6.Certificate.GramData.Block2.entry_7_6 line 398
  99. theorem OAI.MUB6.Certificate.GramData.Block2.entry_7_7 line 402
  100. theorem OAI.MUB6.Certificate.GramData.Block2.entry_7_8 line 406
  101. theorem OAI.MUB6.Certificate.GramData.Block2.entry_7_9 line 410
  102. theorem OAI.MUB6.Certificate.GramData.Block2.entry_7_10 line 414
  103. theorem OAI.MUB6.Certificate.GramData.Block2.entry_8_0 line 418
  104. theorem OAI.MUB6.Certificate.GramData.Block2.entry_8_1 line 422
  105. theorem OAI.MUB6.Certificate.GramData.Block2.entry_8_2 line 426
  106. theorem OAI.MUB6.Certificate.GramData.Block2.entry_8_3 line 430
  107. theorem OAI.MUB6.Certificate.GramData.Block2.entry_8_4 line 434
  108. theorem OAI.MUB6.Certificate.GramData.Block2.entry_8_5 line 438
  109. theorem OAI.MUB6.Certificate.GramData.Block2.entry_8_6 line 442
  110. theorem OAI.MUB6.Certificate.GramData.Block2.entry_8_7 line 446
  111. theorem OAI.MUB6.Certificate.GramData.Block2.entry_8_8 line 450
  112. theorem OAI.MUB6.Certificate.GramData.Block2.entry_8_9 line 454
  113. theorem OAI.MUB6.Certificate.GramData.Block2.entry_8_10 line 458
  114. theorem OAI.MUB6.Certificate.GramData.Block2.entry_9_0 line 462
  115. theorem OAI.MUB6.Certificate.GramData.Block2.entry_9_1 line 466
  116. theorem OAI.MUB6.Certificate.GramData.Block2.entry_9_2 line 470
  117. theorem OAI.MUB6.Certificate.GramData.Block2.entry_9_3 line 474
  118. theorem OAI.MUB6.Certificate.GramData.Block2.entry_9_4 line 478
  119. theorem OAI.MUB6.Certificate.GramData.Block2.entry_9_5 line 482
  120. theorem OAI.MUB6.Certificate.GramData.Block2.entry_9_6 line 486
  121. theorem OAI.MUB6.Certificate.GramData.Block2.entry_9_7 line 490
  122. theorem OAI.MUB6.Certificate.GramData.Block2.entry_9_8 line 494
  123. theorem OAI.MUB6.Certificate.GramData.Block2.entry_9_9 line 498
  124. theorem OAI.MUB6.Certificate.GramData.Block2.entry_9_10 line 502
  125. theorem OAI.MUB6.Certificate.GramData.Block2.entry_10_0 line 506
  126. theorem OAI.MUB6.Certificate.GramData.Block2.entry_10_1 line 510
  127. theorem OAI.MUB6.Certificate.GramData.Block2.entry_10_2 line 514
  128. theorem OAI.MUB6.Certificate.GramData.Block2.entry_10_3 line 518
  129. theorem OAI.MUB6.Certificate.GramData.Block2.entry_10_4 line 522
  130. theorem OAI.MUB6.Certificate.GramData.Block2.entry_10_5 line 526
  131. theorem OAI.MUB6.Certificate.GramData.Block2.entry_10_6 line 530
  132. theorem OAI.MUB6.Certificate.GramData.Block2.entry_10_7 line 534
  133. theorem OAI.MUB6.Certificate.GramData.Block2.entry_10_8 line 538
  134. theorem OAI.MUB6.Certificate.GramData.Block2.entry_10_9 line 542
  135. theorem OAI.MUB6.Certificate.GramData.Block2.entry_10_10 line 546
  136. theorem OAI.MUB6.Certificate.GramData.Block2.pivots_pos line 550
  137. theorem OAI.MUB6.Certificate.GramData.Block2.gram line 565
  138. theorem OAI.MUB6.Certificate.GramData.Block2.positiveDefinite line 691