OAI/Analysis/MutuallyUnbiased/GramRows/Block25.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.rawRow896 line 18
  2. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck896 line 20
  3. def OAI.MUB6.Certificate.GramRows.row896 line 22
  4. theorem OAI.MUB6.Certificate.GramRows.rowCheck896 line 24
  5. theorem OAI.MUB6.Certificate.GramRows.rowEval896 line 27
  6. def OAI.MUB6.Certificate.GramRows.rawRow897 line 31
  7. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck897 line 33
  8. def OAI.MUB6.Certificate.GramRows.row897 line 35
  9. theorem OAI.MUB6.Certificate.GramRows.rowCheck897 line 37
  10. theorem OAI.MUB6.Certificate.GramRows.rowEval897 line 40
  11. def OAI.MUB6.Certificate.GramRows.rawRow898 line 44
  12. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck898 line 46
  13. def OAI.MUB6.Certificate.GramRows.row898 line 48
  14. theorem OAI.MUB6.Certificate.GramRows.rowCheck898 line 50
  15. theorem OAI.MUB6.Certificate.GramRows.rowEval898 line 53
  16. def OAI.MUB6.Certificate.GramRows.rawRow899 line 57
  17. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck899 line 59
  18. def OAI.MUB6.Certificate.GramRows.row899 line 61
  19. theorem OAI.MUB6.Certificate.GramRows.rowCheck899 line 63
  20. theorem OAI.MUB6.Certificate.GramRows.rowEval899 line 66
  21. def OAI.MUB6.Certificate.GramRows.rawRow900 line 70
  22. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck900 line 72
  23. def OAI.MUB6.Certificate.GramRows.row900 line 74
  24. theorem OAI.MUB6.Certificate.GramRows.rowCheck900 line 76
  25. theorem OAI.MUB6.Certificate.GramRows.rowEval900 line 79
  26. def OAI.MUB6.Certificate.GramRows.rawRow901 line 83
  27. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck901 line 85
  28. def OAI.MUB6.Certificate.GramRows.row901 line 87
  29. theorem OAI.MUB6.Certificate.GramRows.rowCheck901 line 89
  30. theorem OAI.MUB6.Certificate.GramRows.rowEval901 line 92
  31. def OAI.MUB6.Certificate.GramRows.rawRow902 line 96
  32. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck902 line 98
  33. def OAI.MUB6.Certificate.GramRows.row902 line 100
  34. theorem OAI.MUB6.Certificate.GramRows.rowCheck902 line 102
  35. theorem OAI.MUB6.Certificate.GramRows.rowEval902 line 105
  36. def OAI.MUB6.Certificate.GramRows.rawRow903 line 109
  37. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck903 line 111
  38. def OAI.MUB6.Certificate.GramRows.row903 line 113
  39. theorem OAI.MUB6.Certificate.GramRows.rowCheck903 line 115
  40. theorem OAI.MUB6.Certificate.GramRows.rowEval903 line 118
  41. def OAI.MUB6.Certificate.GramRows.rawRow904 line 122
  42. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck904 line 124
  43. def OAI.MUB6.Certificate.GramRows.row904 line 126
  44. theorem OAI.MUB6.Certificate.GramRows.rowCheck904 line 128
  45. theorem OAI.MUB6.Certificate.GramRows.rowEval904 line 131
  46. def OAI.MUB6.Certificate.GramRows.rawRow905 line 135
  47. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck905 line 137
  48. def OAI.MUB6.Certificate.GramRows.row905 line 139
  49. theorem OAI.MUB6.Certificate.GramRows.rowCheck905 line 141
  50. theorem OAI.MUB6.Certificate.GramRows.rowEval905 line 144
  51. def OAI.MUB6.Certificate.GramRows.rawRow906 line 148
  52. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck906 line 150
  53. def OAI.MUB6.Certificate.GramRows.row906 line 152
  54. theorem OAI.MUB6.Certificate.GramRows.rowCheck906 line 154
  55. theorem OAI.MUB6.Certificate.GramRows.rowEval906 line 157
  56. def OAI.MUB6.Certificate.GramRows.rawRow907 line 161
  57. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck907 line 163
  58. def OAI.MUB6.Certificate.GramRows.row907 line 165
  59. theorem OAI.MUB6.Certificate.GramRows.rowCheck907 line 167
  60. theorem OAI.MUB6.Certificate.GramRows.rowEval907 line 170
  61. def OAI.MUB6.Certificate.GramRows.rawRow908 line 174
  62. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck908 line 176
  63. def OAI.MUB6.Certificate.GramRows.row908 line 178
  64. theorem OAI.MUB6.Certificate.GramRows.rowCheck908 line 180
  65. theorem OAI.MUB6.Certificate.GramRows.rowEval908 line 183
  66. def OAI.MUB6.Certificate.GramRows.rawRow909 line 187
  67. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck909 line 189
  68. def OAI.MUB6.Certificate.GramRows.row909 line 191
  69. theorem OAI.MUB6.Certificate.GramRows.rowCheck909 line 193
  70. theorem OAI.MUB6.Certificate.GramRows.rowEval909 line 196
  71. def OAI.MUB6.Certificate.GramRows.rawRow910 line 200
  72. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck910 line 202
  73. def OAI.MUB6.Certificate.GramRows.row910 line 204
  74. theorem OAI.MUB6.Certificate.GramRows.rowCheck910 line 206
  75. theorem OAI.MUB6.Certificate.GramRows.rowEval910 line 209
  76. def OAI.MUB6.Certificate.GramRows.rawRow911 line 213
  77. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck911 line 215
  78. def OAI.MUB6.Certificate.GramRows.row911 line 217
  79. theorem OAI.MUB6.Certificate.GramRows.rowCheck911 line 219
  80. theorem OAI.MUB6.Certificate.GramRows.rowEval911 line 222
  81. def OAI.MUB6.Certificate.GramRows.rawRow912 line 226
  82. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck912 line 228
  83. def OAI.MUB6.Certificate.GramRows.row912 line 230
  84. theorem OAI.MUB6.Certificate.GramRows.rowCheck912 line 232
  85. theorem OAI.MUB6.Certificate.GramRows.rowEval912 line 235
  86. def OAI.MUB6.Certificate.GramRows.rawRow913 line 239
  87. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck913 line 241
  88. def OAI.MUB6.Certificate.GramRows.row913 line 243
  89. theorem OAI.MUB6.Certificate.GramRows.rowCheck913 line 245
  90. theorem OAI.MUB6.Certificate.GramRows.rowEval913 line 248
  91. def OAI.MUB6.Certificate.GramRows.rawRow914 line 252
  92. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck914 line 254
  93. def OAI.MUB6.Certificate.GramRows.row914 line 256
  94. theorem OAI.MUB6.Certificate.GramRows.rowCheck914 line 258
  95. theorem OAI.MUB6.Certificate.GramRows.rowEval914 line 261
  96. def OAI.MUB6.Certificate.GramRows.rawRow915 line 265
  97. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck915 line 267
  98. def OAI.MUB6.Certificate.GramRows.row915 line 269
  99. theorem OAI.MUB6.Certificate.GramRows.rowCheck915 line 271
  100. theorem OAI.MUB6.Certificate.GramRows.rowEval915 line 274
  101. def OAI.MUB6.Certificate.GramRows.rawRow916 line 278
  102. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck916 line 280
  103. def OAI.MUB6.Certificate.GramRows.row916 line 282
  104. theorem OAI.MUB6.Certificate.GramRows.rowCheck916 line 284
  105. theorem OAI.MUB6.Certificate.GramRows.rowEval916 line 287
  106. def OAI.MUB6.Certificate.GramRows.rawRow917 line 291
  107. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck917 line 293
  108. def OAI.MUB6.Certificate.GramRows.row917 line 295
  109. theorem OAI.MUB6.Certificate.GramRows.rowCheck917 line 297
  110. theorem OAI.MUB6.Certificate.GramRows.rowEval917 line 300
  111. def OAI.MUB6.Certificate.GramRows.rawRow918 line 304
  112. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck918 line 306
  113. def OAI.MUB6.Certificate.GramRows.row918 line 308
  114. theorem OAI.MUB6.Certificate.GramRows.rowCheck918 line 310
  115. theorem OAI.MUB6.Certificate.GramRows.rowEval918 line 313
  116. def OAI.MUB6.Certificate.GramRows.rawRow919 line 317
  117. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck919 line 319
  118. def OAI.MUB6.Certificate.GramRows.row919 line 321
  119. theorem OAI.MUB6.Certificate.GramRows.rowCheck919 line 323
  120. theorem OAI.MUB6.Certificate.GramRows.rowEval919 line 326
  121. def OAI.MUB6.Certificate.GramRows.rawRow920 line 330
  122. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck920 line 332
  123. def OAI.MUB6.Certificate.GramRows.row920 line 334
  124. theorem OAI.MUB6.Certificate.GramRows.rowCheck920 line 336
  125. theorem OAI.MUB6.Certificate.GramRows.rowEval920 line 339
  126. def OAI.MUB6.Certificate.GramRows.rawRow921 line 343
  127. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck921 line 345
  128. def OAI.MUB6.Certificate.GramRows.row921 line 347
  129. theorem OAI.MUB6.Certificate.GramRows.rowCheck921 line 349
  130. theorem OAI.MUB6.Certificate.GramRows.rowEval921 line 352
  131. def OAI.MUB6.Certificate.GramRows.rawRow922 line 356
  132. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck922 line 358
  133. def OAI.MUB6.Certificate.GramRows.row922 line 360
  134. theorem OAI.MUB6.Certificate.GramRows.rowCheck922 line 362
  135. theorem OAI.MUB6.Certificate.GramRows.rowEval922 line 365
  136. def OAI.MUB6.Certificate.GramRows.rawRow923 line 369
  137. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck923 line 371
  138. def OAI.MUB6.Certificate.GramRows.row923 line 373
  139. theorem OAI.MUB6.Certificate.GramRows.rowCheck923 line 375
  140. theorem OAI.MUB6.Certificate.GramRows.rowEval923 line 378
  141. def OAI.MUB6.Certificate.GramRows.rawRow924 line 382
  142. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck924 line 384
  143. def OAI.MUB6.Certificate.GramRows.row924 line 386
  144. theorem OAI.MUB6.Certificate.GramRows.rowCheck924 line 388
  145. theorem OAI.MUB6.Certificate.GramRows.rowEval924 line 391
  146. def OAI.MUB6.Certificate.GramRows.rawRow925 line 395
  147. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck925 line 397
  148. def OAI.MUB6.Certificate.GramRows.row925 line 399
  149. theorem OAI.MUB6.Certificate.GramRows.rowCheck925 line 401
  150. theorem OAI.MUB6.Certificate.GramRows.rowEval925 line 404
  151. def OAI.MUB6.Certificate.GramRows.rawRow926 line 408
  152. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck926 line 410
  153. def OAI.MUB6.Certificate.GramRows.row926 line 412
  154. theorem OAI.MUB6.Certificate.GramRows.rowCheck926 line 414
  155. theorem OAI.MUB6.Certificate.GramRows.rowEval926 line 417
  156. def OAI.MUB6.Certificate.GramRows.rawRow927 line 421
  157. theorem OAI.MUB6.Certificate.GramRows.rawRowCheck927 line 423
  158. def OAI.MUB6.Certificate.GramRows.row927 line 425
  159. theorem OAI.MUB6.Certificate.GramRows.rowCheck927 line 427
  160. theorem OAI.MUB6.Certificate.GramRows.rowEval927 line 430