OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical158.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5056 line 24
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical5056 line 26
  3. def OAI.MUB6.Certificate.PairSemantics.raw5057 line 30
  4. def OAI.MUB6.Certificate.PairSemantics.raw5057step0 line 32
  5. def OAI.MUB6.Certificate.PairSemantics.raw5057step1 line 34
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical5057 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw5058 line 49
  8. def OAI.MUB6.Certificate.PairSemantics.raw5058step0 line 51
  9. def OAI.MUB6.Certificate.PairSemantics.raw5058step1 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw5058step2 line 55
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5058 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw5059 line 74
  13. def OAI.MUB6.Certificate.PairSemantics.raw5059step0 line 76
  14. def OAI.MUB6.Certificate.PairSemantics.raw5059step1 line 78
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical5059 line 80
  16. def OAI.MUB6.Certificate.PairSemantics.raw5060 line 93
  17. def OAI.MUB6.Certificate.PairSemantics.raw5060step0 line 95
  18. def OAI.MUB6.Certificate.PairSemantics.raw5060step1 line 97
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5060 line 99
  20. def OAI.MUB6.Certificate.PairSemantics.raw5061 line 112
  21. def OAI.MUB6.Certificate.PairSemantics.raw5061step0 line 114
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical5061 line 116
  23. def OAI.MUB6.Certificate.PairSemantics.raw5062 line 125
  24. def OAI.MUB6.Certificate.PairSemantics.raw5062step0 line 127
  25. def OAI.MUB6.Certificate.PairSemantics.raw5062step1 line 129
  26. def OAI.MUB6.Certificate.PairSemantics.raw5062step2 line 131
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical5062 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw5063 line 150
  29. def OAI.MUB6.Certificate.PairSemantics.raw5063step0 line 152
  30. def OAI.MUB6.Certificate.PairSemantics.raw5063step1 line 154
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical5063 line 156
  32. def OAI.MUB6.Certificate.PairSemantics.raw5064 line 169
  33. def OAI.MUB6.Certificate.PairSemantics.raw5064step0 line 171
  34. def OAI.MUB6.Certificate.PairSemantics.raw5064step1 line 173
  35. def OAI.MUB6.Certificate.PairSemantics.raw5064step2 line 175
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5064 line 177
  37. def OAI.MUB6.Certificate.PairSemantics.raw5065 line 194
  38. def OAI.MUB6.Certificate.PairSemantics.raw5065step0 line 196
  39. def OAI.MUB6.Certificate.PairSemantics.raw5065step1 line 198
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical5065 line 200
  41. def OAI.MUB6.Certificate.PairSemantics.raw5066 line 213
  42. def OAI.MUB6.Certificate.PairSemantics.raw5066step0 line 215
  43. def OAI.MUB6.Certificate.PairSemantics.raw5066step1 line 217
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical5066 line 219
  45. def OAI.MUB6.Certificate.PairSemantics.raw5067 line 232
  46. def OAI.MUB6.Certificate.PairSemantics.raw5067step0 line 234
  47. def OAI.MUB6.Certificate.PairSemantics.raw5067step1 line 236
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5067 line 238
  49. def OAI.MUB6.Certificate.PairSemantics.raw5068 line 251
  50. def OAI.MUB6.Certificate.PairSemantics.raw5068step0 line 253
  51. def OAI.MUB6.Certificate.PairSemantics.raw5068step1 line 255
  52. def OAI.MUB6.Certificate.PairSemantics.raw5068step2 line 257
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical5068 line 259
  54. def OAI.MUB6.Certificate.PairSemantics.raw5069 line 276
  55. def OAI.MUB6.Certificate.PairSemantics.raw5069step0 line 278
  56. def OAI.MUB6.Certificate.PairSemantics.raw5069step1 line 280
  57. def OAI.MUB6.Certificate.PairSemantics.raw5069step2 line 282
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical5069 line 284
  59. def OAI.MUB6.Certificate.PairSemantics.raw5070 line 301
  60. def OAI.MUB6.Certificate.PairSemantics.raw5070step0 line 303
  61. def OAI.MUB6.Certificate.PairSemantics.raw5070step1 line 305
  62. def OAI.MUB6.Certificate.PairSemantics.raw5070step2 line 307
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical5070 line 309
  64. def OAI.MUB6.Certificate.PairSemantics.raw5071 line 326
  65. def OAI.MUB6.Certificate.PairSemantics.raw5071step0 line 328
  66. def OAI.MUB6.Certificate.PairSemantics.raw5071step1 line 330
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical5071 line 332
  68. def OAI.MUB6.Certificate.PairSemantics.raw5072 line 345
  69. def OAI.MUB6.Certificate.PairSemantics.raw5072step0 line 347
  70. def OAI.MUB6.Certificate.PairSemantics.raw5072step1 line 349
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical5072 line 351
  72. def OAI.MUB6.Certificate.PairSemantics.raw5073 line 364
  73. def OAI.MUB6.Certificate.PairSemantics.raw5073step0 line 366
  74. def OAI.MUB6.Certificate.PairSemantics.raw5073step1 line 368
  75. def OAI.MUB6.Certificate.PairSemantics.raw5073step2 line 370
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical5073 line 372
  77. def OAI.MUB6.Certificate.PairSemantics.raw5074 line 389
  78. def OAI.MUB6.Certificate.PairSemantics.raw5074step0 line 391
  79. def OAI.MUB6.Certificate.PairSemantics.raw5074step1 line 393
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical5074 line 395
  81. def OAI.MUB6.Certificate.PairSemantics.raw5075 line 408
  82. def OAI.MUB6.Certificate.PairSemantics.raw5075step0 line 410
  83. def OAI.MUB6.Certificate.PairSemantics.raw5075step1 line 412
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5075 line 414
  85. def OAI.MUB6.Certificate.PairSemantics.raw5076 line 427
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical5076 line 429
  87. def OAI.MUB6.Certificate.PairSemantics.raw5077 line 433
  88. def OAI.MUB6.Certificate.PairSemantics.raw5077step0 line 435
  89. def OAI.MUB6.Certificate.PairSemantics.raw5077step1 line 437
  90. def OAI.MUB6.Certificate.PairSemantics.raw5077step2 line 439
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical5077 line 441
  92. def OAI.MUB6.Certificate.PairSemantics.raw5078 line 458
  93. def OAI.MUB6.Certificate.PairSemantics.raw5078step0 line 460
  94. def OAI.MUB6.Certificate.PairSemantics.raw5078step1 line 462
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical5078 line 464
  96. def OAI.MUB6.Certificate.PairSemantics.raw5079 line 477
  97. def OAI.MUB6.Certificate.PairSemantics.raw5079step0 line 479
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical5079 line 481
  99. def OAI.MUB6.Certificate.PairSemantics.raw5080 line 490
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical5080 line 492
  101. def OAI.MUB6.Certificate.PairSemantics.raw5081 line 496
  102. def OAI.MUB6.Certificate.PairSemantics.raw5081step0 line 498
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical5081 line 500
  104. def OAI.MUB6.Certificate.PairSemantics.raw5082 line 509
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical5082 line 511
  106. def OAI.MUB6.Certificate.PairSemantics.raw5083 line 515
  107. def OAI.MUB6.Certificate.PairSemantics.raw5083step0 line 517
  108. def OAI.MUB6.Certificate.PairSemantics.raw5083step1 line 519
  109. def OAI.MUB6.Certificate.PairSemantics.raw5083step2 line 521
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical5083 line 523
  111. def OAI.MUB6.Certificate.PairSemantics.raw5084 line 540
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical5084 line 542
  113. def OAI.MUB6.Certificate.PairSemantics.raw5085 line 546
  114. def OAI.MUB6.Certificate.PairSemantics.raw5085step0 line 548
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical5085 line 550
  116. def OAI.MUB6.Certificate.PairSemantics.raw5086 line 559
  117. def OAI.MUB6.Certificate.PairSemantics.raw5086step0 line 561
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical5086 line 563
  119. def OAI.MUB6.Certificate.PairSemantics.raw5087 line 572
  120. def OAI.MUB6.Certificate.PairSemantics.raw5087step0 line 574
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical5087 line 576