OAI/Analysis/MutuallyUnbiased/MixedSources/Rows100.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1600 line 29
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1600 line 56
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1601 line 61
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1601 line 85
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1602 line 90
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1602 line 114
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1603 line 119
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1603 line 146
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1604 line 151
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1604 line 178
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1605 line 183
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1605 line 207
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1606 line 212
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1606 line 233
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1607 line 238
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1607 line 265
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1608 line 270
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1608 line 297
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1609 line 302
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1609 line 329
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1610 line 334
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1610 line 361
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1611 line 366
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1611 line 393
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1612 line 398
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1612 line 425
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1613 line 430
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1613 line 454
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1614 line 459
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1614 line 483
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1615 line 488
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1615 line 512
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1600 line 517
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1601 line 520
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1602 line 523
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1603 line 526
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1604 line 529
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1605 line 532
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1606 line 535
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1607 line 538
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1608 line 541
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1609 line 544
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1610 line 547
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1611 line 550
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1612 line 553
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1613 line 556
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1614 line 559
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1615 line 562
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound100 line 565