OAI/Analysis/MutuallyUnbiased/MixedSources/Rows63.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1008 line 44
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1008 line 65
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1009 line 70
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1009 line 85
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1010 line 90
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1010 line 111
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1011 line 116
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1011 line 134
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1012 line 139
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1012 line 184
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1013 line 189
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1013 line 234
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1014 line 239
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1014 line 284
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1015 line 289
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1015 line 310
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1016 line 315
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1016 line 339
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1017 line 344
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1017 line 368
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1018 line 373
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1018 line 394
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1019 line 399
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1019 line 420
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1020 line 425
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1020 line 470
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1021 line 475
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1021 line 520
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1022 line 525
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1022 line 546
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1023 line 551
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1023 line 572
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1008 line 577
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1009 line 580
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1010 line 583
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1011 line 586
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1012 line 589
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1013 line 592
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1014 line 595
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1015 line 598
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1016 line 601
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1017 line 604
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1018 line 607
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1019 line 610
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1020 line 613
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1021 line 616
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1022 line 619
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1023 line 622
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound63 line 625