OAI/Analysis/MutuallyUnbiased/MixedSources/Rows21.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero336 line 41
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound336 line 65
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero337 line 70
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound337 line 94
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero338 line 99
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound338 line 123
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero339 line 128
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound339 line 173
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero340 line 178
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound340 line 223
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero341 line 228
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound341 line 273
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero342 line 278
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound342 line 323
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero343 line 328
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound343 line 373
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero344 line 378
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound344 line 423
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero345 line 428
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound345 line 473
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero346 line 478
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound346 line 499
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero347 line 504
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound347 line 525
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero348 line 530
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound348 line 551
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero349 line 556
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound349 line 601
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero350 line 606
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound350 line 627
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero351 line 632
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound351 line 656
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt336 line 661
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt337 line 664
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt338 line 667
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt339 line 670
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt340 line 673
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt341 line 676
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt342 line 679
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt343 line 682
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt344 line 685
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt345 line 688
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt346 line 691
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt347 line 694
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt348 line 697
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt349 line 700
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt350 line 703
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt351 line 706
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound21 line 709