OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary11.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal303 line 47
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix303 line 49
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow303 line 51
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound303 line 53
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal304 line 100
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix304 line 102
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow304 line 104
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound304 line 106
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal305 line 153
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix305 line 155
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow305 line 157
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound305 line 159
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal306 line 206
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix306 line 208
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow306 line 210
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound306 line 212
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal307 line 259
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix307 line 261
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow307 line 263
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound307 line 265
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal308 line 312
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix308 line 314
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow308 line 316
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound308 line 318
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal311 line 365
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix311 line 367
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow311 line 369
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound311 line 371
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal312 line 418
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix312 line 420
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow312 line 422
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound312 line 424
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal313 line 471
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix313 line 473
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow313 line 475
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound313 line 477
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal314 line 524
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix314 line 526
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow314 line 528
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound314 line 530
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal315 line 577
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix315 line 579
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow315 line 581
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound315 line 583
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal332 line 630
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix332 line 632
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow332 line 634
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound332 line 636
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal337 line 683
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix337 line 685
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow337 line 687
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound337 line 689
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal338 line 736
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix338 line 738
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow338 line 740
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound338 line 742
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal339 line 789
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix339 line 791
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow339 line 793
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound339 line 795
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal340 line 842
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix340 line 844
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow340 line 846
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound340 line 848