OAI/Analysis/MutuallyUnbiased/MixedSources/Rows101.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1616 line 34
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1616 line 61
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1617 line 66
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1617 line 90
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1618 line 95
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1618 line 122
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1619 line 127
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1619 line 154
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1620 line 159
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1620 line 186
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1621 line 191
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1621 line 215
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1622 line 220
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1622 line 247
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1623 line 252
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1623 line 276
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1624 line 281
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1624 line 305
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1625 line 310
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1625 line 337
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1626 line 342
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1626 line 369
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1627 line 374
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1627 line 395
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1628 line 400
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1628 line 427
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1629 line 432
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1629 line 456
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1630 line 461
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1630 line 488
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1631 line 493
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1631 line 520
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1616 line 525
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1617 line 528
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1618 line 531
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1619 line 534
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1620 line 537
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1621 line 540
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1622 line 543
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1623 line 546
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1624 line 549
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1625 line 552
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1626 line 555
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1627 line 558
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1628 line 561
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1629 line 564
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1630 line 567
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1631 line 570
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound101 line 573