OAI/Analysis/MutuallyUnbiased/MixedSources/Rows78.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1248 line 37
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1248 line 61
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1249 line 66
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1249 line 87
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1250 line 92
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1250 line 116
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1251 line 121
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1251 line 145
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1252 line 150
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1252 line 177
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1253 line 182
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1253 line 209
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1254 line 214
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1254 line 241
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1255 line 246
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1255 line 270
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1256 line 275
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1256 line 299
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1257 line 304
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1257 line 328
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1258 line 333
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1258 line 354
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1259 line 359
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1259 line 386
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1260 line 391
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1260 line 415
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1261 line 420
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1261 line 465
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1262 line 470
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1262 line 515
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1263 line 520
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1263 line 550
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1248 line 555
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1249 line 558
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1250 line 561
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1251 line 564
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1252 line 567
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1253 line 570
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1254 line 573
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1255 line 576
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1256 line 579
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1257 line 582
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1258 line 585
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1259 line 588
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1260 line 591
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1261 line 594
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1262 line 597
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1263 line 600
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound78 line 603