OAI/Analysis/MutuallyUnbiased/MixedSources/Rows70.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1120 line 57
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1120 line 126
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1121 line 131
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1121 line 200
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1122 line 205
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1122 line 229
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1123 line 234
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1123 line 303
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1124 line 308
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1124 line 377
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1125 line 382
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1125 line 451
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1126 line 456
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1126 line 480
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1127 line 485
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1127 line 509
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1128 line 514
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1128 line 541
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1129 line 546
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1129 line 570
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1130 line 575
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1130 line 644
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1131 line 649
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1131 line 718
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1132 line 723
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1132 line 747
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1133 line 752
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1133 line 776
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1134 line 781
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1134 line 805
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1135 line 810
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1135 line 834
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1120 line 839
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1121 line 842
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1122 line 845
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1123 line 848
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1124 line 851
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1125 line 854
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1126 line 857
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1127 line 860
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1128 line 863
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1129 line 866
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1130 line 869
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1131 line 872
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1132 line 875
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1133 line 878
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1134 line 881
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1135 line 884
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound70 line 887