OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary0.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal0 line 64
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix0 line 66
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow0 line 68
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound0 line 70
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal1 line 117
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix1 line 119
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow1 line 121
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound1 line 123
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal2 line 170
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix2 line 172
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow2 line 174
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound2 line 176
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal3 line 223
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix3 line 225
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow3 line 227
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound3 line 229
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal4 line 276
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix4 line 278
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow4 line 280
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound4 line 282
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal5 line 329
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix5 line 331
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow5 line 333
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound5 line 335
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal6 line 382
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix6 line 384
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow6 line 386
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound6 line 388
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal7 line 435
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix7 line 437
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow7 line 439
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound7 line 441
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal8 line 488
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix8 line 490
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow8 line 492
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound8 line 494
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal9 line 541
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix9 line 543
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow9 line 545
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound9 line 547
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal10 line 594
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix10 line 596
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow10 line 598
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound10 line 600
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal11 line 647
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix11 line 649
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow11 line 651
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound11 line 653
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal12 line 700
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix12 line 702
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow12 line 704
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound12 line 706
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal13 line 753
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix13 line 755
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow13 line 757
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound13 line 759
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal14 line 806
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix14 line 808
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow14 line 810
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound14 line 812
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal16 line 859
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix16 line 861
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow16 line 863
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound16 line 865