OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary15.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal408 line 45
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix408 line 47
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow408 line 49
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound408 line 51
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal409 line 98
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix409 line 100
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow409 line 102
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound409 line 104
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal410 line 151
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix410 line 153
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow410 line 155
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound410 line 157
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal412 line 204
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix412 line 206
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow412 line 208
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound412 line 210
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal419 line 257
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix419 line 259
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow419 line 261
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound419 line 263
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal422 line 310
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix422 line 312
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow422 line 314
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound422 line 316
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal423 line 363
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix423 line 365
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow423 line 367
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound423 line 369
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal425 line 416
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix425 line 418
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow425 line 420
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound425 line 422
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal430 line 469
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix430 line 471
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow430 line 473
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound430 line 475
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal433 line 522
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix433 line 524
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow433 line 526
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound433 line 528
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal434 line 575
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix434 line 577
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow434 line 579
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound434 line 581
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal436 line 628
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix436 line 630
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow436 line 632
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound436 line 634
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal444 line 681
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix444 line 683
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow444 line 685
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound444 line 687
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal445 line 734
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix445 line 736
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow445 line 738
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound445 line 740
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal446 line 787
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix446 line 789
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow446 line 791
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound446 line 793
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal447 line 840
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix447 line 842
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow447 line 844
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound447 line 846