OAI/Analysis/MutuallyUnbiased/MixedSources/Rows16.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero256 line 38
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound256 line 65
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero257 line 70
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound257 line 97
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero258 line 102
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound258 line 126
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero259 line 131
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound259 line 158
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero260 line 163
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound260 line 190
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero261 line 195
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound261 line 222
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero262 line 227
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound262 line 254
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero263 line 259
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound263 line 286
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero264 line 291
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound264 line 315
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero265 line 320
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound265 line 344
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero266 line 349
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound266 line 376
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero267 line 381
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound267 line 471
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero268 line 476
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound268 line 572
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero269 line 577
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound269 line 673
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero270 line 678
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound270 line 705
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero271 line 710
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound271 line 737
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt256 line 742
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt257 line 745
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt258 line 748
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt259 line 751
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt260 line 754
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt261 line 757
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt262 line 760
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt263 line 763
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt264 line 766
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt265 line 769
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt266 line 772
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt267 line 775
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt268 line 778
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt269 line 781
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt270 line 784
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt271 line 787
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound16 line 790