OAI/Analysis/MutuallyUnbiased/MixedSources/Rows31.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero496 line 51
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound496 line 75
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero497 line 80
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound497 line 176
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero498 line 181
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound498 line 277
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero499 line 282
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound499 line 360
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero500 line 365
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound500 line 458
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero501 line 463
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound501 line 556
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero502 line 561
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound502 line 588
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero503 line 593
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound503 line 689
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero504 line 694
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound504 line 790
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero505 line 795
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound505 line 891
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero506 line 896
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound506 line 923
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero507 line 928
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound507 line 955
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero508 line 960
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound508 line 987
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero509 line 992
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound509 line 1019
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero510 line 1024
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound510 line 1048
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero511 line 1053
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound511 line 1080
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt496 line 1085
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt497 line 1088
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt498 line 1091
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt499 line 1094
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt500 line 1097
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt501 line 1100
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt502 line 1103
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt503 line 1106
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt504 line 1109
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt505 line 1112
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt506 line 1115
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt507 line 1118
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt508 line 1121
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt509 line 1124
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt510 line 1127
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt511 line 1130
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound31 line 1133