OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary7.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal140 line 34
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix140 line 36
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow140 line 38
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound140 line 40
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal144 line 87
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix144 line 89
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow144 line 91
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound144 line 93
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal145 line 140
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix145 line 142
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow145 line 144
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound145 line 146
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal146 line 193
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix146 line 195
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow146 line 197
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound146 line 199
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal147 line 246
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix147 line 248
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow147 line 250
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound147 line 252
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal150 line 299
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix150 line 301
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow150 line 303
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound150 line 305
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal151 line 352
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix151 line 354
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow151 line 356
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound151 line 358
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal152 line 405
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix152 line 407
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow152 line 409
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound152 line 411
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal153 line 458
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix153 line 460
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow153 line 462
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound153 line 464
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal156 line 511
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix156 line 513
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow156 line 515
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound156 line 517
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal157 line 564
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix157 line 566
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow157 line 568
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound157 line 570
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal158 line 617
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix158 line 619
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow158 line 621
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound158 line 623
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal161 line 670
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix161 line 672
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow161 line 674
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound161 line 676
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal162 line 723
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix162 line 725
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow162 line 727
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound162 line 729
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal165 line 776
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix165 line 778
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow165 line 780
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound165 line 782
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal166 line 829
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix166 line 831
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow166 line 833
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound166 line 835