OAI/Analysis/MutuallyUnbiased/MixedSources/Rows88.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1408 line 35
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1408 line 59
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1409 line 64
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1409 line 112
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1410 line 117
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1410 line 165
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1411 line 170
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1411 line 218
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1412 line 223
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1412 line 271
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1413 line 276
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1413 line 324
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1414 line 329
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1414 line 377
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1415 line 382
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1415 line 403
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1416 line 408
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1416 line 432
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1417 line 437
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1417 line 503
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1418 line 508
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1418 line 574
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1419 line 579
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1419 line 621
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1420 line 626
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1420 line 692
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1421 line 697
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1421 line 763
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1422 line 768
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1422 line 837
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1423 line 842
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1423 line 911
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1408 line 916
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1409 line 919
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1410 line 922
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1411 line 925
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1412 line 928
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1413 line 931
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1414 line 934
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1415 line 937
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1416 line 940
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1417 line 943
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1418 line 946
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1419 line 949
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1420 line 952
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1421 line 955
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1422 line 958
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1423 line 961
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound88 line 964