OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary4.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal68 line 56
  2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix68 line 58
  3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow68 line 60
  4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound68 line 62
  5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal69 line 109
  6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix69 line 111
  7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow69 line 113
  8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound69 line 115
  9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal70 line 162
  10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix70 line 164
  11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow70 line 166
  12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound70 line 168
  13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal71 line 215
  14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix71 line 217
  15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow71 line 219
  16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound71 line 221
  17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal72 line 268
  18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix72 line 270
  19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow72 line 272
  20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound72 line 274
  21. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal73 line 321
  22. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix73 line 323
  23. def OAI.MUB6.Certificate.PairSemantics.boundaryRow73 line 325
  24. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound73 line 327
  25. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal74 line 374
  26. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix74 line 376
  27. def OAI.MUB6.Certificate.PairSemantics.boundaryRow74 line 378
  28. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound74 line 380
  29. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal75 line 427
  30. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix75 line 429
  31. def OAI.MUB6.Certificate.PairSemantics.boundaryRow75 line 431
  32. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound75 line 433
  33. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal77 line 480
  34. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix77 line 482
  35. def OAI.MUB6.Certificate.PairSemantics.boundaryRow77 line 484
  36. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound77 line 486
  37. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal78 line 533
  38. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix78 line 535
  39. def OAI.MUB6.Certificate.PairSemantics.boundaryRow78 line 537
  40. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound78 line 539
  41. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal79 line 586
  42. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix79 line 588
  43. def OAI.MUB6.Certificate.PairSemantics.boundaryRow79 line 590
  44. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound79 line 592
  45. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal80 line 639
  46. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix80 line 641
  47. def OAI.MUB6.Certificate.PairSemantics.boundaryRow80 line 643
  48. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound80 line 645
  49. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal81 line 692
  50. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix81 line 694
  51. def OAI.MUB6.Certificate.PairSemantics.boundaryRow81 line 696
  52. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound81 line 698
  53. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal82 line 745
  54. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix82 line 747
  55. def OAI.MUB6.Certificate.PairSemantics.boundaryRow82 line 749
  56. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound82 line 751
  57. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal83 line 798
  58. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix83 line 800
  59. def OAI.MUB6.Certificate.PairSemantics.boundaryRow83 line 802
  60. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound83 line 804
  61. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal84 line 851
  62. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix84 line 853
  63. def OAI.MUB6.Certificate.PairSemantics.boundaryRow84 line 855
  64. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound84 line 857