OAI/Analysis/MutuallyUnbiased/MixedSources/Rows77.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1232 line 38
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1232 line 83
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1233 line 88
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1233 line 133
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1234 line 138
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1234 line 183
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1235 line 188
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1235 line 212
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1236 line 217
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1236 line 241
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1237 line 246
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1237 line 270
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1238 line 275
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1238 line 296
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1239 line 301
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1239 line 325
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1240 line 330
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1240 line 357
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1241 line 362
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1241 line 389
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1242 line 394
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1242 line 418
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1243 line 423
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1243 line 444
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1244 line 449
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1244 line 473
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1245 line 478
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1245 line 502
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1246 line 507
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1246 line 531
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1247 line 536
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1247 line 560
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1232 line 565
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1233 line 568
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1234 line 571
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1235 line 574
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1236 line 577
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1237 line 580
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1238 line 583
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1239 line 586
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1240 line 589
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1241 line 592
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1242 line 595
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1243 line 598
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1244 line 601
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1245 line 604
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1246 line 607
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1247 line 610
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound77 line 613