OAI/Analysis/MutuallyUnbiased/MixedSources/Rows67.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1072 line 33
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1072 line 57
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1073 line 62
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1073 line 83
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1074 line 88
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1074 line 112
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1075 line 117
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1075 line 141
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1076 line 146
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1076 line 170
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1077 line 175
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1077 line 202
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1078 line 207
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1078 line 234
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1079 line 239
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1079 line 263
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1080 line 268
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1080 line 295
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1081 line 300
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1081 line 327
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1082 line 332
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1082 line 359
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1083 line 364
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1083 line 388
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1084 line 393
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1084 line 417
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1085 line 422
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1085 line 449
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1086 line 454
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1086 line 481
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1087 line 486
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1087 line 513
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1072 line 518
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1073 line 521
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1074 line 524
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1075 line 527
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1076 line 530
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1077 line 533
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1078 line 536
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1079 line 539
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1080 line 542
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1081 line 545
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1082 line 548
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1083 line 551
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1084 line 554
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1085 line 557
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1086 line 560
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1087 line 563
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound67 line 566