OAI/Analysis/MutuallyUnbiased/MixedSources/Rows15.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero240 line 42
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound240 line 66
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero241 line 71
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound241 line 98
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero242 line 103
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound242 line 130
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero243 line 135
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound243 line 162
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero244 line 167
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound244 line 263
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero245 line 268
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound245 line 364
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero246 line 369
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound246 line 396
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero247 line 401
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound247 line 428
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero248 line 433
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound248 line 460
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero249 line 465
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound249 line 492
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero250 line 497
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound250 line 521
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero251 line 526
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound251 line 553
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero252 line 558
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound252 line 585
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero253 line 590
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound253 line 617
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero254 line 622
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound254 line 649
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero255 line 654
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound255 line 747
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt240 line 752
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt241 line 755
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt242 line 758
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt243 line 761
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt244 line 764
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt245 line 767
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt246 line 770
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt247 line 773
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt248 line 776
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt249 line 779
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt250 line 782
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt251 line 785
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt252 line 788
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt253 line 791
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt254 line 794
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt255 line 797
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound15 line 800