OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary14.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal390 line 37
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix390 line 39
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow390 line 41
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound390 line 43
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal393 line 90
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix393 line 92
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow393 line 94
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound393 line 96
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal394 line 143
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix394 line 145
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow394 line 147
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound394 line 149
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal395 line 196
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix395 line 198
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow395 line 200
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound395 line 202
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal396 line 249
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix396 line 251
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow396 line 253
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound396 line 255
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal397 line 302
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix397 line 304
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow397 line 306
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound397 line 308
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal398 line 355
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix398 line 357
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow398 line 359
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound398 line 361
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal399 line 408
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix399 line 410
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow399 line 412
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound399 line 414
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal400 line 461
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix400 line 463
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow400 line 465
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound400 line 467
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal401 line 514
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix401 line 516
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow401 line 518
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound401 line 520
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal402 line 567
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix402 line 569
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow402 line 571
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound402 line 573
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal403 line 620
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix403 line 622
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow403 line 624
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound403 line 626
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal404 line 673
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix404 line 675
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow404 line 677
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound404 line 679
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal405 line 726
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix405 line 728
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow405 line 730
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound405 line 732
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal406 line 779
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix406 line 781
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow406 line 783
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound406 line 785
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal407 line 832
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix407 line 834
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow407 line 836
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound407 line 838