OAI/Analysis/MutuallyUnbiased/GramRows/Block18.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow672 line 22
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck672 line 24
  3. def OAI.MUB6.Certificate.GramRows.row672 line 26
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck672 line 28
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval672 line 31
  6. def OAI.MUB6.Certificate.GramRows.rawRow673 line 35
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck673 line 37
  8. def OAI.MUB6.Certificate.GramRows.row673 line 39
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck673 line 41
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval673 line 44
  11. def OAI.MUB6.Certificate.GramRows.rawRow674 line 48
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck674 line 50
  13. def OAI.MUB6.Certificate.GramRows.row674 line 52
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck674 line 54
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval674 line 57
  16. def OAI.MUB6.Certificate.GramRows.rawRow675 line 61
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck675 line 63
  18. def OAI.MUB6.Certificate.GramRows.row675 line 65
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck675 line 67
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval675 line 70
  21. def OAI.MUB6.Certificate.GramRows.rawRow676 line 74
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck676 line 76
  23. def OAI.MUB6.Certificate.GramRows.row676 line 78
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck676 line 80
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval676 line 83
  26. def OAI.MUB6.Certificate.GramRows.rawRow677 line 87
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck677 line 89
  28. def OAI.MUB6.Certificate.GramRows.row677 line 91
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck677 line 93
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval677 line 96
  31. def OAI.MUB6.Certificate.GramRows.rawRow678 line 100
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck678 line 102
  33. def OAI.MUB6.Certificate.GramRows.row678 line 104
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck678 line 106
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval678 line 109
  36. def OAI.MUB6.Certificate.GramRows.rawRow679 line 113
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck679 line 115
  38. def OAI.MUB6.Certificate.GramRows.row679 line 117
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck679 line 119
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval679 line 122
  41. def OAI.MUB6.Certificate.GramRows.rawRow680 line 126
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck680 line 128
  43. def OAI.MUB6.Certificate.GramRows.row680 line 130
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck680 line 132
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval680 line 135
  46. def OAI.MUB6.Certificate.GramRows.rawRow681 line 139
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck681 line 141
  48. def OAI.MUB6.Certificate.GramRows.row681 line 143
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck681 line 145
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval681 line 148
  51. def OAI.MUB6.Certificate.GramRows.rawRow682 line 152
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck682 line 154
  53. def OAI.MUB6.Certificate.GramRows.row682 line 156
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck682 line 158
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval682 line 161
  56. def OAI.MUB6.Certificate.GramRows.rawRow683 line 165
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck683 line 167
  58. def OAI.MUB6.Certificate.GramRows.row683 line 169
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck683 line 171
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval683 line 174
  61. def OAI.MUB6.Certificate.GramRows.rawRow684 line 178
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck684 line 180
  63. def OAI.MUB6.Certificate.GramRows.row684 line 182
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck684 line 184
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval684 line 187
  66. def OAI.MUB6.Certificate.GramRows.rawRow685 line 191
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck685 line 193
  68. def OAI.MUB6.Certificate.GramRows.row685 line 195
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck685 line 197
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval685 line 200
  71. def OAI.MUB6.Certificate.GramRows.rawRow686 line 204
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck686 line 206
  73. def OAI.MUB6.Certificate.GramRows.row686 line 208
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck686 line 210
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval686 line 213
  76. def OAI.MUB6.Certificate.GramRows.rawRow687 line 217
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck687 line 219
  78. def OAI.MUB6.Certificate.GramRows.row687 line 221
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck687 line 223
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval687 line 226
  81. def OAI.MUB6.Certificate.GramRows.rawRow688 line 230
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck688 line 232
  83. def OAI.MUB6.Certificate.GramRows.row688 line 234
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck688 line 236
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval688 line 239
  86. def OAI.MUB6.Certificate.GramRows.rawRow689 line 243
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck689 line 245
  88. def OAI.MUB6.Certificate.GramRows.row689 line 247
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck689 line 249
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval689 line 252
  91. def OAI.MUB6.Certificate.GramRows.rawRow690 line 256
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck690 line 258
  93. def OAI.MUB6.Certificate.GramRows.row690 line 260
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck690 line 262
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval690 line 265
  96. def OAI.MUB6.Certificate.GramRows.rawRow691 line 269
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck691 line 271
  98. def OAI.MUB6.Certificate.GramRows.row691 line 273
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck691 line 275
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval691 line 278
  101. def OAI.MUB6.Certificate.GramRows.rawRow692 line 282
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck692 line 284
  103. def OAI.MUB6.Certificate.GramRows.row692 line 286
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck692 line 288
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval692 line 291
  106. def OAI.MUB6.Certificate.GramRows.rawRow693 line 295
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck693 line 297
  108. def OAI.MUB6.Certificate.GramRows.row693 line 299
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck693 line 301
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval693 line 304
  111. def OAI.MUB6.Certificate.GramRows.rawRow694 line 308
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck694 line 310
  113. def OAI.MUB6.Certificate.GramRows.row694 line 312
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck694 line 314
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval694 line 317
  116. def OAI.MUB6.Certificate.GramRows.rawRow695 line 321
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck695 line 323
  118. def OAI.MUB6.Certificate.GramRows.row695 line 325
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck695 line 327
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval695 line 330
  121. def OAI.MUB6.Certificate.GramRows.rawRow696 line 334
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck696 line 336
  123. def OAI.MUB6.Certificate.GramRows.row696 line 338
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck696 line 340
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval696 line 343
  126. def OAI.MUB6.Certificate.GramRows.rawRow697 line 347
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck697 line 349
  128. def OAI.MUB6.Certificate.GramRows.row697 line 351
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck697 line 353
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval697 line 356
  131. def OAI.MUB6.Certificate.GramRows.rawRow698 line 360
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck698 line 362
  133. def OAI.MUB6.Certificate.GramRows.row698 line 364
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck698 line 366
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval698 line 369
  136. def OAI.MUB6.Certificate.GramRows.rawRow699 line 373
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck699 line 375
  138. def OAI.MUB6.Certificate.GramRows.row699 line 377
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck699 line 379
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval699 line 382
  141. def OAI.MUB6.Certificate.GramRows.rawRow700 line 386
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck700 line 388
  143. def OAI.MUB6.Certificate.GramRows.row700 line 390
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck700 line 392
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval700 line 395
  146. def OAI.MUB6.Certificate.GramRows.rawRow701 line 399
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck701 line 401
  148. def OAI.MUB6.Certificate.GramRows.row701 line 403
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck701 line 405
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval701 line 408
  151. def OAI.MUB6.Certificate.GramRows.rawRow702 line 412
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck702 line 414
  153. def OAI.MUB6.Certificate.GramRows.row702 line 416
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck702 line 418
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval702 line 421
  156. def OAI.MUB6.Certificate.GramRows.rawRow703 line 425
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck703 line 427
  158. def OAI.MUB6.Certificate.GramRows.row703 line 429
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck703 line 431
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval703 line 434