OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary5.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal85 line 41
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix85 line 43
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow85 line 45
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound85 line 47
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal87 line 94
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix87 line 96
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow87 line 98
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound87 line 100
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal88 line 147
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix88 line 149
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow88 line 151
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound88 line 153
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal89 line 200
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix89 line 202
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow89 line 204
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound89 line 206
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal90 line 253
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix90 line 255
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow90 line 257
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound90 line 259
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal91 line 306
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix91 line 308
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow91 line 310
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound91 line 312
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal92 line 359
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix92 line 361
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow92 line 363
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound92 line 365
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal93 line 412
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix93 line 414
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow93 line 416
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound93 line 418
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal94 line 465
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix94 line 467
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow94 line 469
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound94 line 471
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal95 line 518
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix95 line 520
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow95 line 522
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound95 line 524
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal96 line 571
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix96 line 573
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow96 line 575
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound96 line 577
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal97 line 624
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix97 line 626
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow97 line 628
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound97 line 630
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal98 line 677
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix98 line 679
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow98 line 681
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound98 line 683
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal99 line 730
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix99 line 732
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow99 line 734
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound99 line 736
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal100 line 783
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix100 line 785
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow100 line 787
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound100 line 789
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal101 line 836
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix101 line 838
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow101 line 840
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound101 line 842