OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary3.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal49 line 43
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix49 line 45
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow49 line 47
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound49 line 49
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal50 line 96
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix50 line 98
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow50 line 100
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound50 line 102
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal51 line 149
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix51 line 151
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow51 line 153
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound51 line 155
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal52 line 202
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix52 line 204
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow52 line 206
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound52 line 208
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal53 line 255
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix53 line 257
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow53 line 259
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound53 line 261
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal54 line 308
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix54 line 310
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow54 line 312
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound54 line 314
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal55 line 361
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix55 line 363
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow55 line 365
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound55 line 367
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal56 line 414
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix56 line 416
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow56 line 418
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound56 line 420
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal57 line 467
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix57 line 469
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow57 line 471
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound57 line 473
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal58 line 520
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix58 line 522
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow58 line 524
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound58 line 526
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal59 line 573
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix59 line 575
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow59 line 577
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound59 line 579
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal60 line 626
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix60 line 628
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow60 line 630
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound60 line 632
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal64 line 679
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix64 line 681
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow64 line 683
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound64 line 685
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal65 line 732
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix65 line 734
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow65 line 736
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound65 line 738
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal66 line 785
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix66 line 787
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow66 line 789
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound66 line 791
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal67 line 838
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix67 line 840
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow67 line 842
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound67 line 844