OAI/Analysis/MutuallyUnbiased/MixedSources/Rows72.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1152 line 50
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1152 line 74
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1153 line 79
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1153 line 103
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1154 line 108
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1154 line 132
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1155 line 137
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1155 line 161
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1156 line 166
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1156 line 190
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1157 line 195
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1157 line 219
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1158 line 224
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1158 line 293
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1159 line 298
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1159 line 367
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1160 line 372
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1160 line 441
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1161 line 446
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1161 line 470
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1162 line 475
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1162 line 496
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1163 line 501
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1163 line 525
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1164 line 530
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1164 line 557
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1165 line 562
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1165 line 631
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1166 line 636
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1166 line 705
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1167 line 710
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1167 line 779
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1152 line 784
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1153 line 787
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1154 line 790
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1155 line 793
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1156 line 796
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1157 line 799
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1158 line 802
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1159 line 805
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1160 line 808
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1161 line 811
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1162 line 814
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1163 line 817
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1164 line 820
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1165 line 823
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1166 line 826
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1167 line 829
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound72 line 832