OAI/Analysis/MutuallyUnbiased/MixedSources/Rows79.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1264 line 40
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1264 line 85
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1265 line 90
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1265 line 111
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1266 line 116
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1266 line 146
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1267 line 151
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1267 line 181
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1268 line 186
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1268 line 207
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1269 line 212
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1269 line 242
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1270 line 247
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1270 line 265
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1271 line 270
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1271 line 339
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1272 line 344
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1272 line 413
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1273 line 418
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1273 line 487
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1274 line 492
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1274 line 516
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1275 line 521
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1275 line 548
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1276 line 553
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1276 line 580
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1277 line 585
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1277 line 609
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1278 line 614
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1278 line 683
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1279 line 688
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1279 line 757
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1264 line 762
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1265 line 765
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1266 line 768
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1267 line 771
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1268 line 774
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1269 line 777
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1270 line 780
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1271 line 783
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1272 line 786
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1273 line 789
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1274 line 792
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1275 line 795
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1276 line 798
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1277 line 801
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1278 line 804
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1279 line 807
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound79 line 810