OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound9.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.PairSemantics.sound576 line 32
  2. theorem OAI.MUB6.Certificate.PairSemantics.sound577 line 37
  3. theorem OAI.MUB6.Certificate.PairSemantics.sound578 line 42
  4. theorem OAI.MUB6.Certificate.PairSemantics.sound579 line 47
  5. theorem OAI.MUB6.Certificate.PairSemantics.sound580 line 52
  6. theorem OAI.MUB6.Certificate.PairSemantics.sound581 line 57
  7. theorem OAI.MUB6.Certificate.PairSemantics.sound582 line 62
  8. theorem OAI.MUB6.Certificate.PairSemantics.sound583 line 67
  9. theorem OAI.MUB6.Certificate.PairSemantics.sound584 line 72
  10. theorem OAI.MUB6.Certificate.PairSemantics.sound585 line 77
  11. theorem OAI.MUB6.Certificate.PairSemantics.sound586 line 82
  12. theorem OAI.MUB6.Certificate.PairSemantics.sound587 line 87
  13. theorem OAI.MUB6.Certificate.PairSemantics.sound588 line 92
  14. theorem OAI.MUB6.Certificate.PairSemantics.sound589 line 97
  15. theorem OAI.MUB6.Certificate.PairSemantics.sound590 line 102
  16. theorem OAI.MUB6.Certificate.PairSemantics.sound591 line 107
  17. theorem OAI.MUB6.Certificate.PairSemantics.sound592 line 112
  18. theorem OAI.MUB6.Certificate.PairSemantics.sound593 line 117
  19. theorem OAI.MUB6.Certificate.PairSemantics.sound594 line 122
  20. theorem OAI.MUB6.Certificate.PairSemantics.sound595 line 127
  21. theorem OAI.MUB6.Certificate.PairSemantics.sound596 line 132
  22. theorem OAI.MUB6.Certificate.PairSemantics.sound597 line 137
  23. theorem OAI.MUB6.Certificate.PairSemantics.sound598 line 142
  24. theorem OAI.MUB6.Certificate.PairSemantics.sound599 line 147
  25. theorem OAI.MUB6.Certificate.PairSemantics.sound600 line 152
  26. theorem OAI.MUB6.Certificate.PairSemantics.sound601 line 157
  27. theorem OAI.MUB6.Certificate.PairSemantics.sound602 line 162
  28. theorem OAI.MUB6.Certificate.PairSemantics.sound603 line 167
  29. theorem OAI.MUB6.Certificate.PairSemantics.sound604 line 172
  30. theorem OAI.MUB6.Certificate.PairSemantics.sound605 line 177
  31. theorem OAI.MUB6.Certificate.PairSemantics.sound606 line 182
  32. theorem OAI.MUB6.Certificate.PairSemantics.sound607 line 187
  33. theorem OAI.MUB6.Certificate.PairSemantics.sound608 line 192
  34. theorem OAI.MUB6.Certificate.PairSemantics.sound609 line 197
  35. theorem OAI.MUB6.Certificate.PairSemantics.sound610 line 202
  36. theorem OAI.MUB6.Certificate.PairSemantics.sound611 line 207
  37. theorem OAI.MUB6.Certificate.PairSemantics.sound612 line 212
  38. theorem OAI.MUB6.Certificate.PairSemantics.sound613 line 217
  39. theorem OAI.MUB6.Certificate.PairSemantics.sound614 line 222
  40. theorem OAI.MUB6.Certificate.PairSemantics.sound615 line 227
  41. theorem OAI.MUB6.Certificate.PairSemantics.sound616 line 232
  42. theorem OAI.MUB6.Certificate.PairSemantics.sound617 line 237
  43. theorem OAI.MUB6.Certificate.PairSemantics.sound618 line 242
  44. theorem OAI.MUB6.Certificate.PairSemantics.sound619 line 247
  45. theorem OAI.MUB6.Certificate.PairSemantics.sound620 line 252
  46. theorem OAI.MUB6.Certificate.PairSemantics.sound621 line 257
  47. theorem OAI.MUB6.Certificate.PairSemantics.sound622 line 262
  48. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation623 line 267
  49. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix623 line 273
  50. theorem OAI.MUB6.Certificate.PairSemantics.sound623 line 275
  51. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation624 line 310
  52. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix624 line 316
  53. theorem OAI.MUB6.Certificate.PairSemantics.sound624 line 318
  54. theorem OAI.MUB6.Certificate.PairSemantics.sound625 line 353
  55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation626 line 358
  56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix626 line 364
  57. theorem OAI.MUB6.Certificate.PairSemantics.sound626 line 366
  58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation627 line 401
  59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix627 line 407
  60. theorem OAI.MUB6.Certificate.PairSemantics.sound627 line 409
  61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation628 line 444
  62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix628 line 450
  63. theorem OAI.MUB6.Certificate.PairSemantics.sound628 line 452
  64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation629 line 487
  65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix629 line 493
  66. theorem OAI.MUB6.Certificate.PairSemantics.sound629 line 495
  67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation630 line 530
  68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix630 line 536
  69. theorem OAI.MUB6.Certificate.PairSemantics.sound630 line 538
  70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation631 line 573
  71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix631 line 579
  72. theorem OAI.MUB6.Certificate.PairSemantics.sound631 line 581
  73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation632 line 616
  74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix632 line 622
  75. theorem OAI.MUB6.Certificate.PairSemantics.sound632 line 624
  76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation633 line 659
  77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix633 line 665
  78. theorem OAI.MUB6.Certificate.PairSemantics.sound633 line 667
  79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation634 line 702
  80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix634 line 708
  81. theorem OAI.MUB6.Certificate.PairSemantics.sound634 line 710
  82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation635 line 745
  83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix635 line 751
  84. theorem OAI.MUB6.Certificate.PairSemantics.sound635 line 753
  85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation636 line 788
  86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix636 line 794
  87. theorem OAI.MUB6.Certificate.PairSemantics.sound636 line 796
  88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation637 line 831
  89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix637 line 837
  90. theorem OAI.MUB6.Certificate.PairSemantics.sound637 line 839
  91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation638 line 874
  92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix638 line 880
  93. theorem OAI.MUB6.Certificate.PairSemantics.sound638 line 882
  94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation639 line 917
  95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix639 line 923
  96. theorem OAI.MUB6.Certificate.PairSemantics.sound639 line 925