OAI/Analysis/MutuallyUnbiased/MixedSources/Rows10.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero160 line 33
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound160 line 60
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero161 line 65
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound161 line 92
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero162 line 97
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound162 line 121
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero163 line 126
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound163 line 222
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero164 line 227
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound164 line 248
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero165 line 253
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound165 line 274
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero166 line 279
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound166 line 300
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero167 line 305
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound167 line 326
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero168 line 331
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound168 line 358
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero169 line 363
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound169 line 390
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero170 line 395
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound170 line 422
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero171 line 427
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound171 line 448
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero172 line 453
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound172 line 474
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero173 line 479
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound173 line 503
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero174 line 508
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound174 line 532
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero175 line 537
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound175 line 555
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt160 line 560
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt161 line 563
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt162 line 566
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt163 line 569
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt164 line 572
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt165 line 575
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt166 line 578
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt167 line 581
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt168 line 584
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt169 line 587
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt170 line 590
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt171 line 593
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt172 line 596
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt173 line 599
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt174 line 602
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt175 line 605
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound10 line 608