OAI/Analysis/MutuallyUnbiased/MixedSources/Rows91.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1456 line 39
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1456 line 66
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1457 line 71
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1457 line 95
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1458 line 100
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1458 line 121
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1459 line 126
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1459 line 147
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1460 line 152
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1460 line 176
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1461 line 181
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1461 line 205
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1462 line 210
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1462 line 237
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1463 line 242
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1463 line 269
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1464 line 274
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1464 line 301
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1465 line 306
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1465 line 375
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1466 line 380
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1466 line 449
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1467 line 454
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1467 line 475
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1468 line 480
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1468 line 504
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1469 line 509
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1469 line 578
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1470 line 583
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1470 line 652
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1471 line 657
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1471 line 747
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1456 line 752
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1457 line 755
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1458 line 758
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1459 line 761
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1460 line 764
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1461 line 767
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1462 line 770
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1463 line 773
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1464 line 776
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1465 line 779
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1466 line 782
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1467 line 785
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1468 line 788
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1469 line 791
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1470 line 794
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1471 line 797
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound91 line 800