OAI/Analysis/MutuallyUnbiased/MixedSources/Rows82.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1312 line 48
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1312 line 96
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1313 line 101
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1313 line 128
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1314 line 133
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1314 line 160
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1315 line 165
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1315 line 192
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1316 line 197
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1316 line 224
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1317 line 229
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1317 line 274
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1318 line 279
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1318 line 324
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1319 line 329
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1319 line 374
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1320 line 379
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1320 line 400
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1321 line 405
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1321 line 450
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1322 line 455
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1322 line 500
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1323 line 505
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1323 line 526
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1324 line 531
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1324 line 576
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1325 line 581
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1325 line 605
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1326 line 610
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1326 line 658
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1327 line 663
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1327 line 684
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1312 line 689
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1313 line 692
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1314 line 695
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1315 line 698
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1316 line 701
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1317 line 704
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1318 line 707
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1319 line 710
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1320 line 713
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1321 line 716
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1322 line 719
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1323 line 722
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1324 line 725
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1325 line 728
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1326 line 731
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1327 line 734
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound82 line 737