OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary13.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal369 line 36
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix369 line 38
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow369 line 40
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound369 line 42
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal372 line 89
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix372 line 91
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow372 line 93
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound372 line 95
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal373 line 142
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix373 line 144
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow373 line 146
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound373 line 148
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal374 line 195
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix374 line 197
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow374 line 199
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound374 line 201
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal377 line 248
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix377 line 250
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow377 line 252
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound377 line 254
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal378 line 301
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix378 line 303
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow378 line 305
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound378 line 307
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal379 line 354
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix379 line 356
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow379 line 358
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound379 line 360
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal381 line 407
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix381 line 409
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow381 line 411
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound381 line 413
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal382 line 460
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix382 line 462
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow382 line 464
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound382 line 466
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal383 line 513
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix383 line 515
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow383 line 517
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound383 line 519
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal384 line 566
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix384 line 568
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow384 line 570
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound384 line 572
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal385 line 619
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix385 line 621
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow385 line 623
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound385 line 625
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal386 line 672
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix386 line 674
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow386 line 676
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound386 line 678
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal387 line 725
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix387 line 727
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow387 line 729
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound387 line 731
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal388 line 778
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix388 line 780
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow388 line 782
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound388 line 784
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal389 line 831
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix389 line 833
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow389 line 835
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound389 line 837