OAI/Analysis/MutuallyUnbiased/MixedSources/Rows64.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1024 line 38
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1024 line 59
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1025 line 64
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1025 line 85
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1026 line 90
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1026 line 111
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1027 line 116
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1027 line 140
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1028 line 145
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1028 line 166
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1029 line 171
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1029 line 195
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1030 line 200
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1030 line 221
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1031 line 226
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1031 line 247
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1032 line 252
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1032 line 270
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1033 line 275
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1033 line 296
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1034 line 301
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1034 line 346
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1035 line 351
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1035 line 396
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1036 line 401
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1036 line 422
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1037 line 427
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1037 line 451
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1038 line 456
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1038 line 477
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1039 line 482
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1039 line 503
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1024 line 508
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1025 line 511
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1026 line 514
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1027 line 517
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1028 line 520
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1029 line 523
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1030 line 526
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1031 line 529
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1032 line 532
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1033 line 535
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1034 line 538
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1035 line 541
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1036 line 544
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1037 line 547
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1038 line 550
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1039 line 553
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound64 line 556