OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary12.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal343 line 41
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix343 line 43
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow343 line 45
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound343 line 47
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal345 line 94
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix345 line 96
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow345 line 98
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound345 line 100
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal346 line 147
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix346 line 149
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow346 line 151
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound346 line 153
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal347 line 200
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix347 line 202
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow347 line 204
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound347 line 206
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal349 line 253
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix349 line 255
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow349 line 257
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound349 line 259
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal350 line 306
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix350 line 308
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow350 line 310
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound350 line 312
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal351 line 359
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix351 line 361
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow351 line 363
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound351 line 365
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal353 line 412
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix353 line 414
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow353 line 416
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound353 line 418
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal354 line 465
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix354 line 467
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow354 line 469
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound354 line 471
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal355 line 518
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix355 line 520
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow355 line 522
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound355 line 524
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal356 line 571
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix356 line 573
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow356 line 575
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound356 line 577
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal362 line 624
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix362 line 626
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow362 line 628
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound362 line 630
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal363 line 677
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix363 line 679
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow363 line 681
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound363 line 683
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal364 line 730
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix364 line 732
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow364 line 734
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound364 line 736
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal365 line 783
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix365 line 785
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow365 line 787
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound365 line 789
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal368 line 836
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix368 line 838
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow368 line 840
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound368 line 842