OAI/Analysis/MutuallyUnbiased/MixedSources/Rows95.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1520 line 31
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1520 line 52
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1521 line 57
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1521 line 105
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1522 line 110
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1522 line 137
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1523 line 142
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1523 line 169
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1524 line 174
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1524 line 198
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1525 line 203
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1525 line 227
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1526 line 232
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1526 line 259
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1527 line 264
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1527 line 288
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1528 line 293
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1528 line 320
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1529 line 325
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1529 line 352
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1530 line 357
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1530 line 384
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1531 line 389
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1531 line 410
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1532 line 415
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1532 line 436
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1533 line 441
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1533 line 462
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1534 line 467
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1534 line 491
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1535 line 496
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1535 line 520
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1520 line 525
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1521 line 528
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1522 line 531
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1523 line 534
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1524 line 537
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1525 line 540
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1526 line 543
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1527 line 546
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1528 line 549
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1529 line 552
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1530 line 555
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1531 line 558
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1532 line 561
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1533 line 564
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1534 line 567
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1535 line 570
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound95 line 573