OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary2.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal33 line 62
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix33 line 64
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow33 line 66
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound33 line 68
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal34 line 115
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix34 line 117
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow34 line 119
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound34 line 121
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal35 line 168
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix35 line 170
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow35 line 172
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound35 line 174
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal36 line 221
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix36 line 223
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow36 line 225
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound36 line 227
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal37 line 274
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix37 line 276
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow37 line 278
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound37 line 280
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal38 line 327
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix38 line 329
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow38 line 331
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound38 line 333
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal39 line 380
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix39 line 382
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow39 line 384
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound39 line 386
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal40 line 433
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix40 line 435
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow40 line 437
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound40 line 439
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal41 line 486
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix41 line 488
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow41 line 490
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound41 line 492
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal42 line 539
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix42 line 541
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow42 line 543
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound42 line 545
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal43 line 592
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix43 line 594
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow43 line 596
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound43 line 598
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal44 line 645
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix44 line 647
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow44 line 649
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound44 line 651
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal45 line 698
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix45 line 700
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow45 line 702
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound45 line 704
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal46 line 751
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix46 line 753
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow46 line 755
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound46 line 757
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal47 line 804
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix47 line 806
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow47 line 808
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound47 line 810
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal48 line 857
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix48 line 859
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow48 line 861
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound48 line 863