OAI/Analysis/MutuallyUnbiased/MixedSources/Rows71.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1136 line 33
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1136 line 57
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1137 line 62
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1137 line 86
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1138 line 91
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1138 line 115
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1139 line 120
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1139 line 144
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1140 line 149
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1140 line 173
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1141 line 178
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1141 line 202
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1142 line 207
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1142 line 231
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1143 line 236
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1143 line 263
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1144 line 268
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1144 line 292
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1145 line 297
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1145 line 321
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1146 line 326
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1146 line 350
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1147 line 355
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1147 line 379
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1148 line 384
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1148 line 411
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1149 line 416
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1149 line 443
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1150 line 448
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1150 line 475
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1151 line 480
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1151 line 507
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1136 line 512
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1137 line 515
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1138 line 518
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1139 line 521
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1140 line 524
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1141 line 527
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1142 line 530
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1143 line 533
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1144 line 536
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1145 line 539
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1146 line 542
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1147 line 545
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1148 line 548
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1149 line 551
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1150 line 554
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1151 line 557
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound71 line 560