OAI/Analysis/MutuallyUnbiased/MixedSources/Rows109.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1744 line 37
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1744 line 82
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1745 line 87
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1745 line 114
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1746 line 119
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1746 line 146
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1747 line 151
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1747 line 178
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1748 line 183
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1748 line 207
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1749 line 212
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1749 line 236
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1750 line 241
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1750 line 265
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1751 line 270
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1751 line 297
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1752 line 302
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1752 line 329
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1753 line 334
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1753 line 361
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1754 line 366
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1754 line 390
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1755 line 395
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1755 line 419
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1756 line 424
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1756 line 448
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1757 line 453
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1757 line 477
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1758 line 482
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1758 line 509
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1759 line 514
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1759 line 541
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1744 line 546
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1745 line 549
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1746 line 552
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1747 line 555
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1748 line 558
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1749 line 561
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1750 line 564
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1751 line 567
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1752 line 570
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1753 line 573
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1754 line 576
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1755 line 579
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1756 line 582
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1757 line 585
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1758 line 588
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1759 line 591
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound109 line 594