OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary9.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal246 line 45
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix246 line 47
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow246 line 49
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound246 line 51
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal247 line 98
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix247 line 100
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow247 line 102
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound247 line 104
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal248 line 151
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix248 line 153
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow248 line 155
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound248 line 157
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal249 line 204
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix249 line 206
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow249 line 208
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound249 line 210
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal250 line 257
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix250 line 259
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow250 line 261
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound250 line 263
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal251 line 310
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix251 line 312
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow251 line 314
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound251 line 316
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal252 line 363
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix252 line 365
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow252 line 367
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound252 line 369
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal253 line 416
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix253 line 418
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow253 line 420
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound253 line 422
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal261 line 469
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix261 line 471
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow261 line 473
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound261 line 475
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal262 line 522
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix262 line 524
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow262 line 526
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound262 line 528
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal263 line 575
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix263 line 577
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow263 line 579
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound263 line 581
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal264 line 628
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix264 line 630
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow264 line 632
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound264 line 634
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal265 line 681
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix265 line 683
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow265 line 685
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound265 line 687
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal266 line 734
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix266 line 736
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow266 line 738
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound266 line 740
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal267 line 787
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix267 line 789
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow267 line 791
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound267 line 793
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal268 line 840
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix268 line 842
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow268 line 844
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound268 line 846