OAI/Analysis/MutuallyUnbiased/GramRows/Block4.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow224 line 18
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck224 line 20
  3. def OAI.MUB6.Certificate.GramRows.row224 line 22
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck224 line 24
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval224 line 27
  6. def OAI.MUB6.Certificate.GramRows.rawRow225 line 31
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck225 line 33
  8. def OAI.MUB6.Certificate.GramRows.row225 line 35
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck225 line 37
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval225 line 40
  11. def OAI.MUB6.Certificate.GramRows.rawRow226 line 44
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck226 line 46
  13. def OAI.MUB6.Certificate.GramRows.row226 line 48
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck226 line 50
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval226 line 53
  16. def OAI.MUB6.Certificate.GramRows.rawRow227 line 57
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck227 line 59
  18. def OAI.MUB6.Certificate.GramRows.row227 line 61
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck227 line 63
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval227 line 66
  21. def OAI.MUB6.Certificate.GramRows.rawRow228 line 70
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck228 line 72
  23. def OAI.MUB6.Certificate.GramRows.row228 line 74
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck228 line 76
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval228 line 79
  26. def OAI.MUB6.Certificate.GramRows.rawRow229 line 83
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck229 line 85
  28. def OAI.MUB6.Certificate.GramRows.row229 line 87
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck229 line 89
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval229 line 92
  31. def OAI.MUB6.Certificate.GramRows.rawRow230 line 96
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck230 line 98
  33. def OAI.MUB6.Certificate.GramRows.row230 line 100
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck230 line 102
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval230 line 105
  36. def OAI.MUB6.Certificate.GramRows.rawRow231 line 109
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck231 line 111
  38. def OAI.MUB6.Certificate.GramRows.row231 line 113
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck231 line 115
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval231 line 118
  41. def OAI.MUB6.Certificate.GramRows.rawRow232 line 122
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck232 line 124
  43. def OAI.MUB6.Certificate.GramRows.row232 line 126
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck232 line 128
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval232 line 131
  46. def OAI.MUB6.Certificate.GramRows.rawRow233 line 135
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck233 line 137
  48. def OAI.MUB6.Certificate.GramRows.row233 line 139
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck233 line 141
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval233 line 144
  51. def OAI.MUB6.Certificate.GramRows.rawRow234 line 148
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck234 line 150
  53. def OAI.MUB6.Certificate.GramRows.row234 line 152
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck234 line 154
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval234 line 157
  56. def OAI.MUB6.Certificate.GramRows.rawRow235 line 161
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck235 line 163
  58. def OAI.MUB6.Certificate.GramRows.row235 line 165
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck235 line 167
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval235 line 170
  61. def OAI.MUB6.Certificate.GramRows.rawRow236 line 174
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck236 line 176
  63. def OAI.MUB6.Certificate.GramRows.row236 line 178
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck236 line 180
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval236 line 183
  66. def OAI.MUB6.Certificate.GramRows.rawRow237 line 187
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck237 line 189
  68. def OAI.MUB6.Certificate.GramRows.row237 line 191
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck237 line 193
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval237 line 196
  71. def OAI.MUB6.Certificate.GramRows.rawRow238 line 200
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck238 line 202
  73. def OAI.MUB6.Certificate.GramRows.row238 line 204
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck238 line 206
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval238 line 209
  76. def OAI.MUB6.Certificate.GramRows.rawRow239 line 213
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck239 line 215
  78. def OAI.MUB6.Certificate.GramRows.row239 line 217
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck239 line 219
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval239 line 222
  81. def OAI.MUB6.Certificate.GramRows.rawRow240 line 226
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck240 line 228
  83. def OAI.MUB6.Certificate.GramRows.row240 line 230
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck240 line 232
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval240 line 235
  86. def OAI.MUB6.Certificate.GramRows.rawRow241 line 239
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck241 line 241
  88. def OAI.MUB6.Certificate.GramRows.row241 line 243
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck241 line 245
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval241 line 248
  91. def OAI.MUB6.Certificate.GramRows.rawRow242 line 252
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck242 line 254
  93. def OAI.MUB6.Certificate.GramRows.row242 line 256
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck242 line 258
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval242 line 261
  96. def OAI.MUB6.Certificate.GramRows.rawRow243 line 265
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck243 line 267
  98. def OAI.MUB6.Certificate.GramRows.row243 line 269
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck243 line 271
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval243 line 274
  101. def OAI.MUB6.Certificate.GramRows.rawRow244 line 278
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck244 line 280
  103. def OAI.MUB6.Certificate.GramRows.row244 line 282
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck244 line 284
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval244 line 287
  106. def OAI.MUB6.Certificate.GramRows.rawRow245 line 291
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck245 line 293
  108. def OAI.MUB6.Certificate.GramRows.row245 line 295
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck245 line 297
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval245 line 300
  111. def OAI.MUB6.Certificate.GramRows.rawRow246 line 304
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck246 line 306
  113. def OAI.MUB6.Certificate.GramRows.row246 line 308
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck246 line 310
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval246 line 313
  116. def OAI.MUB6.Certificate.GramRows.rawRow247 line 317
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck247 line 319
  118. def OAI.MUB6.Certificate.GramRows.row247 line 321
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck247 line 323
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval247 line 326
  121. def OAI.MUB6.Certificate.GramRows.rawRow248 line 330
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck248 line 332
  123. def OAI.MUB6.Certificate.GramRows.row248 line 334
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck248 line 336
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval248 line 339
  126. def OAI.MUB6.Certificate.GramRows.rawRow249 line 343
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck249 line 345
  128. def OAI.MUB6.Certificate.GramRows.row249 line 347
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck249 line 349
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval249 line 352
  131. def OAI.MUB6.Certificate.GramRows.rawRow250 line 356
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck250 line 358
  133. def OAI.MUB6.Certificate.GramRows.row250 line 360
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck250 line 362
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval250 line 365
  136. def OAI.MUB6.Certificate.GramRows.rawRow251 line 369
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck251 line 371
  138. def OAI.MUB6.Certificate.GramRows.row251 line 373
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck251 line 375
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval251 line 378
  141. def OAI.MUB6.Certificate.GramRows.rawRow252 line 382
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck252 line 384
  143. def OAI.MUB6.Certificate.GramRows.row252 line 386
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck252 line 388
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval252 line 391
  146. def OAI.MUB6.Certificate.GramRows.rawRow253 line 395
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck253 line 397
  148. def OAI.MUB6.Certificate.GramRows.row253 line 399
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck253 line 401
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval253 line 404
  151. def OAI.MUB6.Certificate.GramRows.rawRow254 line 408
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck254 line 410
  153. def OAI.MUB6.Certificate.GramRows.row254 line 412
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck254 line 414
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval254 line 417
  156. def OAI.MUB6.Certificate.GramRows.rawRow255 line 421
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck255 line 423
  158. def OAI.MUB6.Certificate.GramRows.row255 line 425
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck255 line 427
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval255 line 430