OAI/Analysis/MutuallyUnbiased/MixedSources/Rows5.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero80 line 43
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound80 line 67
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero81 line 72
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound81 line 96
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero82 line 101
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound82 line 125
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero83 line 130
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound83 line 157
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero84 line 162
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound84 line 189
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero85 line 194
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound85 line 218
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero86 line 223
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound86 line 247
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero87 line 252
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound87 line 276
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero88 line 281
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound88 line 299
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero89 line 304
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound89 line 325
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero90 line 330
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound90 line 348
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero91 line 353
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound91 line 398
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero92 line 403
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound92 line 448
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero93 line 453
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound93 line 483
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero94 line 488
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound94 line 533
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero95 line 538
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound95 line 559
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt80 line 564
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt81 line 567
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt82 line 570
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt83 line 573
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt84 line 576
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt85 line 579
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt86 line 582
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt87 line 585
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt88 line 588
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt89 line 591
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt90 line 594
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt91 line 597
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt92 line 600
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt93 line 603
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt94 line 606
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt95 line 609
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound5 line 612