OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary6.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal102 line 39
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix102 line 41
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow102 line 43
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound102 line 45
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal103 line 92
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix103 line 94
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow103 line 96
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound103 line 98
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal104 line 145
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix104 line 147
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow104 line 149
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound104 line 151
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal105 line 198
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix105 line 200
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow105 line 202
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound105 line 204
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal106 line 251
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix106 line 253
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow106 line 255
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound106 line 257
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal107 line 304
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix107 line 306
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow107 line 308
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound107 line 310
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal108 line 357
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix108 line 359
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow108 line 361
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound108 line 363
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal128 line 410
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix128 line 412
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow128 line 414
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound128 line 416
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal129 line 463
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix129 line 465
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow129 line 467
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound129 line 469
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal130 line 516
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix130 line 518
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow130 line 520
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound130 line 522
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal131 line 569
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix131 line 571
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow131 line 573
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound131 line 575
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal133 line 622
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix133 line 624
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow133 line 626
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound133 line 628
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal134 line 675
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix134 line 677
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow134 line 679
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound134 line 681
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal135 line 728
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix135 line 730
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow135 line 732
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound135 line 734
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal138 line 781
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix138 line 783
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow138 line 785
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound138 line 787
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal139 line 834
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix139 line 836
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow139 line 838
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound139 line 840