OAI/Analysis/MutuallyUnbiased/GramRows/Block9.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow384 line 14
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck384 line 16
  3. def OAI.MUB6.Certificate.GramRows.row384 line 18
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck384 line 20
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval384 line 23
  6. def OAI.MUB6.Certificate.GramRows.rawRow385 line 27
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck385 line 29
  8. def OAI.MUB6.Certificate.GramRows.row385 line 31
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck385 line 33
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval385 line 36
  11. def OAI.MUB6.Certificate.GramRows.rawRow386 line 40
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck386 line 42
  13. def OAI.MUB6.Certificate.GramRows.row386 line 44
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck386 line 46
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval386 line 49
  16. def OAI.MUB6.Certificate.GramRows.rawRow387 line 53
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck387 line 55
  18. def OAI.MUB6.Certificate.GramRows.row387 line 57
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck387 line 59
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval387 line 62
  21. def OAI.MUB6.Certificate.GramRows.rawRow388 line 66
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck388 line 68
  23. def OAI.MUB6.Certificate.GramRows.row388 line 70
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck388 line 72
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval388 line 75
  26. def OAI.MUB6.Certificate.GramRows.rawRow389 line 79
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck389 line 81
  28. def OAI.MUB6.Certificate.GramRows.row389 line 83
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck389 line 85
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval389 line 88
  31. def OAI.MUB6.Certificate.GramRows.rawRow390 line 92
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck390 line 94
  33. def OAI.MUB6.Certificate.GramRows.row390 line 96
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck390 line 98
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval390 line 101
  36. def OAI.MUB6.Certificate.GramRows.rawRow391 line 105
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck391 line 107
  38. def OAI.MUB6.Certificate.GramRows.row391 line 109
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck391 line 111
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval391 line 114
  41. def OAI.MUB6.Certificate.GramRows.rawRow392 line 118
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck392 line 120
  43. def OAI.MUB6.Certificate.GramRows.row392 line 122
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck392 line 124
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval392 line 127
  46. def OAI.MUB6.Certificate.GramRows.rawRow393 line 131
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck393 line 133
  48. def OAI.MUB6.Certificate.GramRows.row393 line 135
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck393 line 137
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval393 line 140
  51. def OAI.MUB6.Certificate.GramRows.rawRow394 line 144
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck394 line 146
  53. def OAI.MUB6.Certificate.GramRows.row394 line 148
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck394 line 150
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval394 line 153
  56. def OAI.MUB6.Certificate.GramRows.rawRow395 line 157
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck395 line 159
  58. def OAI.MUB6.Certificate.GramRows.row395 line 161
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck395 line 163
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval395 line 166
  61. def OAI.MUB6.Certificate.GramRows.rawRow396 line 170
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck396 line 172
  63. def OAI.MUB6.Certificate.GramRows.row396 line 174
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck396 line 176
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval396 line 179
  66. def OAI.MUB6.Certificate.GramRows.rawRow397 line 183
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck397 line 185
  68. def OAI.MUB6.Certificate.GramRows.row397 line 187
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck397 line 189
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval397 line 192
  71. def OAI.MUB6.Certificate.GramRows.rawRow398 line 196
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck398 line 198
  73. def OAI.MUB6.Certificate.GramRows.row398 line 200
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck398 line 202
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval398 line 205
  76. def OAI.MUB6.Certificate.GramRows.rawRow399 line 209
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck399 line 211
  78. def OAI.MUB6.Certificate.GramRows.row399 line 213
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck399 line 215
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval399 line 218
  81. def OAI.MUB6.Certificate.GramRows.rawRow400 line 222
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck400 line 224
  83. def OAI.MUB6.Certificate.GramRows.row400 line 226
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck400 line 228
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval400 line 231
  86. def OAI.MUB6.Certificate.GramRows.rawRow401 line 235
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck401 line 237
  88. def OAI.MUB6.Certificate.GramRows.row401 line 239
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck401 line 241
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval401 line 244
  91. def OAI.MUB6.Certificate.GramRows.rawRow402 line 248
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck402 line 250
  93. def OAI.MUB6.Certificate.GramRows.row402 line 252
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck402 line 254
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval402 line 257
  96. def OAI.MUB6.Certificate.GramRows.rawRow403 line 261
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck403 line 263
  98. def OAI.MUB6.Certificate.GramRows.row403 line 265
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck403 line 267
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval403 line 270
  101. def OAI.MUB6.Certificate.GramRows.rawRow404 line 274
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck404 line 276
  103. def OAI.MUB6.Certificate.GramRows.row404 line 278
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck404 line 280
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval404 line 283
  106. def OAI.MUB6.Certificate.GramRows.rawRow405 line 287
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck405 line 289
  108. def OAI.MUB6.Certificate.GramRows.row405 line 291
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck405 line 293
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval405 line 296
  111. def OAI.MUB6.Certificate.GramRows.rawRow406 line 300
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck406 line 302
  113. def OAI.MUB6.Certificate.GramRows.row406 line 304
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck406 line 306
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval406 line 309
  116. def OAI.MUB6.Certificate.GramRows.rawRow407 line 313
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck407 line 315
  118. def OAI.MUB6.Certificate.GramRows.row407 line 317
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck407 line 319
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval407 line 322
  121. def OAI.MUB6.Certificate.GramRows.rawRow408 line 326
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck408 line 328
  123. def OAI.MUB6.Certificate.GramRows.row408 line 330
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck408 line 332
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval408 line 335
  126. def OAI.MUB6.Certificate.GramRows.rawRow409 line 339
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck409 line 341
  128. def OAI.MUB6.Certificate.GramRows.row409 line 343
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck409 line 345
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval409 line 348
  131. def OAI.MUB6.Certificate.GramRows.rawRow410 line 352
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck410 line 354
  133. def OAI.MUB6.Certificate.GramRows.row410 line 356
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck410 line 358
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval410 line 361
  136. def OAI.MUB6.Certificate.GramRows.rawRow411 line 365
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck411 line 367
  138. def OAI.MUB6.Certificate.GramRows.row411 line 369
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck411 line 371
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval411 line 374
  141. def OAI.MUB6.Certificate.GramRows.rawRow412 line 378
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck412 line 380
  143. def OAI.MUB6.Certificate.GramRows.row412 line 382
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck412 line 384
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval412 line 387
  146. def OAI.MUB6.Certificate.GramRows.rawRow413 line 391
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck413 line 393
  148. def OAI.MUB6.Certificate.GramRows.row413 line 395
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck413 line 397
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval413 line 400
  151. def OAI.MUB6.Certificate.GramRows.rawRow414 line 404
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck414 line 406
  153. def OAI.MUB6.Certificate.GramRows.row414 line 408
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck414 line 410
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval414 line 413
  156. def OAI.MUB6.Certificate.GramRows.rawRow415 line 417
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck415 line 419
  158. def OAI.MUB6.Certificate.GramRows.row415 line 421
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck415 line 423
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval415 line 426