OAI/Analysis/MutuallyUnbiased/GramData/Block5.lean

GitHub source file

162 declarations, 0 contain sorry, 0 declared as axioms

Exact integer matrix for λ = (5,), m = 12, exponent = 15.

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