OAI/Analysis/MutuallyUnbiased/MixedSources/Rows76.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1216 line 29
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1216 line 50
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1217 line 55
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1217 line 79
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1218 line 84
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1218 line 108
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1219 line 113
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1219 line 137
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1220 line 142
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1220 line 166
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1221 line 171
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1221 line 198
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1222 line 203
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1222 line 227
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1223 line 232
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1223 line 256
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1224 line 261
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1224 line 285
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1225 line 290
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1225 line 314
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1226 line 319
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1226 line 343
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1227 line 348
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1227 line 417
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1228 line 422
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1228 line 491
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1229 line 496
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1229 line 520
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1230 line 525
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1230 line 549
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1231 line 554
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1231 line 623
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1216 line 628
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1217 line 631
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1218 line 634
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1219 line 637
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1220 line 640
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1221 line 643
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1222 line 646
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1223 line 649
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1224 line 652
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1225 line 655
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1226 line 658
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1227 line 661
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1228 line 664
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1229 line 667
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1230 line 670
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1231 line 673
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound76 line 676