OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary1.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal17 line 63
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix17 line 65
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow17 line 67
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound17 line 69
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal18 line 116
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix18 line 118
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow18 line 120
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound18 line 122
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal19 line 169
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix19 line 171
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow19 line 173
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound19 line 175
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal20 line 222
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix20 line 224
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow20 line 226
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound20 line 228
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal21 line 275
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix21 line 277
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow21 line 279
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound21 line 281
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal22 line 328
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix22 line 330
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow22 line 332
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound22 line 334
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal23 line 381
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix23 line 383
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow23 line 385
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound23 line 387
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal24 line 434
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix24 line 436
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow24 line 438
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound24 line 440
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal25 line 487
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix25 line 489
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow25 line 491
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound25 line 493
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal26 line 540
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix26 line 542
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow26 line 544
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound26 line 546
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal27 line 593
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix27 line 595
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow27 line 597
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound27 line 599
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal28 line 646
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix28 line 648
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow28 line 650
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound28 line 652
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal29 line 699
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix29 line 701
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow29 line 703
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound29 line 705
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal30 line 752
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix30 line 754
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow30 line 756
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound30 line 758
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal31 line 805
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix31 line 807
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow31 line 809
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound31 line 811
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal32 line 858
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix32 line 860
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow32 line 862
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound32 line 864