OAI/Analysis/MutuallyUnbiased/MixedSources/Rows66.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1056 line 37
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1056 line 61
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1057 line 66
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1057 line 90
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1058 line 95
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1058 line 119
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1059 line 124
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1059 line 151
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1060 line 156
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1060 line 183
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1061 line 188
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1061 line 212
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1062 line 217
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1062 line 241
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1063 line 246
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1063 line 270
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1064 line 275
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1064 line 299
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1065 line 304
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1065 line 331
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1066 line 336
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1066 line 360
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1067 line 365
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1067 line 392
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1068 line 397
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1068 line 421
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1069 line 426
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1069 line 450
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1070 line 455
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1070 line 479
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1071 line 484
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1071 line 508
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1056 line 513
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1057 line 516
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1058 line 519
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1059 line 522
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1060 line 525
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1061 line 528
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1062 line 531
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1063 line 534
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1064 line 537
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1065 line 540
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1066 line 543
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1067 line 546
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1068 line 549
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1069 line 552
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1070 line 555
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1071 line 558
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound66 line 561