OAI/Analysis/MutuallyUnbiased/MixedSources/Rows28.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero448 line 48
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound448 line 117
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero449 line 122
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound449 line 146
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero450 line 151
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound450 line 175
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero451 line 180
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound451 line 204
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero452 line 209
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound452 line 278
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero453 line 283
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound453 line 352
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero454 line 357
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound454 line 426
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero455 line 431
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound455 line 455
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero456 line 460
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound456 line 529
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero457 line 534
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound457 line 558
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero458 line 563
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound458 line 587
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero459 line 592
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound459 line 616
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero460 line 621
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound460 line 645
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero461 line 650
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound461 line 719
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero462 line 724
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound462 line 793
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero463 line 798
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound463 line 867
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt448 line 872
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt449 line 875
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt450 line 878
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt451 line 881
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt452 line 884
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt453 line 887
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt454 line 890
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt455 line 893
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt456 line 896
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt457 line 899
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt458 line 902
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt459 line 905
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt460 line 908
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt461 line 911
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt462 line 914
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt463 line 917
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound28 line 920