OAI/Analysis/MutuallyUnbiased/MixedSources/Rows80.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1280 line 47
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1280 line 71
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1281 line 76
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1281 line 97
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1282 line 102
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1282 line 123
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1283 line 128
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1283 line 152
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1284 line 157
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1284 line 178
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1285 line 183
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1285 line 207
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1286 line 212
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1286 line 236
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1287 line 241
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1287 line 268
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1288 line 273
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1288 line 297
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1289 line 302
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1289 line 326
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1290 line 331
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1290 line 355
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1291 line 360
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1291 line 381
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1292 line 386
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1292 line 410
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1293 line 415
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1293 line 484
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1294 line 489
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1294 line 558
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1295 line 563
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1295 line 632
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1280 line 637
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1281 line 640
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1282 line 643
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1283 line 646
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1284 line 649
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1285 line 652
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1286 line 655
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1287 line 658
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1288 line 661
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1289 line 664
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1290 line 667
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1291 line 670
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1292 line 673
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1293 line 676
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1294 line 679
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1295 line 682
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound80 line 685