OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary10.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal269 line 58
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix269 line 60
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow269 line 62
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound269 line 64
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal270 line 111
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix270 line 113
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow270 line 115
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound270 line 117
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal271 line 164
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix271 line 166
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow271 line 168
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound271 line 170
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal273 line 217
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix273 line 219
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow273 line 221
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound273 line 223
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal275 line 270
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix275 line 272
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow275 line 274
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound275 line 276
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal276 line 323
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix276 line 325
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow276 line 327
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound276 line 329
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal277 line 376
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix277 line 378
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow277 line 380
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound277 line 382
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal278 line 429
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix278 line 431
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow278 line 433
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound278 line 435
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal285 line 482
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix285 line 484
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow285 line 486
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound285 line 488
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal286 line 535
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix286 line 537
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow286 line 539
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound286 line 541
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal287 line 588
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix287 line 590
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow287 line 592
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound287 line 594
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal297 line 641
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix297 line 643
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow297 line 645
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound297 line 647
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal298 line 694
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix298 line 696
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow298 line 698
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound298 line 700
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal300 line 747
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix300 line 749
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow300 line 751
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound300 line 753
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal301 line 800
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix301 line 802
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow301 line 804
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound301 line 806
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal302 line 853
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix302 line 855
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow302 line 857
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound302 line 859