OAI/Analysis/MutuallyUnbiased/MixedSources/Rows18.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero288 line 39
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound288 line 66
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero289 line 71
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound289 line 98
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero290 line 103
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound290 line 130
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero291 line 135
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound291 line 162
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero292 line 167
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound292 line 191
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero293 line 196
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound293 line 223
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero294 line 228
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound294 line 255
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero295 line 260
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound295 line 287
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero296 line 292
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound296 line 388
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero297 line 393
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound297 line 420
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero298 line 425
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound298 line 452
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero299 line 457
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound299 line 484
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero300 line 489
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound300 line 516
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero301 line 521
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound301 line 590
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero302 line 595
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound302 line 619
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero303 line 624
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound303 line 648
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt288 line 653
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt289 line 656
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt290 line 659
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt291 line 662
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt292 line 665
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt293 line 668
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt294 line 671
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt295 line 674
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt296 line 677
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt297 line 680
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt298 line 683
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt299 line 686
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt300 line 689
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt301 line 692
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt302 line 695
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt303 line 698
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound18 line 701