OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical164.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5248 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw5248step0 line 19
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical5248 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw5249 line 30
  5. def OAI.MUB6.Certificate.PairSemantics.raw5249step0 line 32
  6. def OAI.MUB6.Certificate.PairSemantics.raw5249step1 line 34
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical5249 line 36
  8. def OAI.MUB6.Certificate.PairSemantics.raw5250 line 49
  9. def OAI.MUB6.Certificate.PairSemantics.raw5250step0 line 51
  10. def OAI.MUB6.Certificate.PairSemantics.raw5250step1 line 53
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5250 line 55
  12. def OAI.MUB6.Certificate.PairSemantics.raw5251 line 68
  13. def OAI.MUB6.Certificate.PairSemantics.raw5251step0 line 70
  14. def OAI.MUB6.Certificate.PairSemantics.raw5251step1 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw5251step2 line 74
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical5251 line 76
  17. def OAI.MUB6.Certificate.PairSemantics.raw5252 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw5252step0 line 95
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5252 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw5253 line 106
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical5253 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw5254 line 112
  23. def OAI.MUB6.Certificate.PairSemantics.raw5254step0 line 114
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical5254 line 116
  25. def OAI.MUB6.Certificate.PairSemantics.raw5255 line 125
  26. def OAI.MUB6.Certificate.PairSemantics.raw5255step0 line 127
  27. def OAI.MUB6.Certificate.PairSemantics.raw5255step1 line 129
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical5255 line 131
  29. def OAI.MUB6.Certificate.PairSemantics.raw5256 line 144
  30. def OAI.MUB6.Certificate.PairSemantics.raw5256step0 line 146
  31. def OAI.MUB6.Certificate.PairSemantics.raw5256step1 line 148
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5256 line 150
  33. def OAI.MUB6.Certificate.PairSemantics.raw5257 line 163
  34. def OAI.MUB6.Certificate.PairSemantics.raw5257step0 line 165
  35. def OAI.MUB6.Certificate.PairSemantics.raw5257step1 line 167
  36. def OAI.MUB6.Certificate.PairSemantics.raw5257step2 line 169
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical5257 line 171
  38. def OAI.MUB6.Certificate.PairSemantics.raw5258 line 188
  39. def OAI.MUB6.Certificate.PairSemantics.raw5258step0 line 190
  40. def OAI.MUB6.Certificate.PairSemantics.raw5258step1 line 192
  41. def OAI.MUB6.Certificate.PairSemantics.raw5258step2 line 194
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical5258 line 196
  43. def OAI.MUB6.Certificate.PairSemantics.raw5259 line 213
  44. def OAI.MUB6.Certificate.PairSemantics.raw5259step0 line 215
  45. def OAI.MUB6.Certificate.PairSemantics.raw5259step1 line 217
  46. def OAI.MUB6.Certificate.PairSemantics.raw5259step2 line 219
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical5259 line 221
  48. def OAI.MUB6.Certificate.PairSemantics.raw5260 line 238
  49. def OAI.MUB6.Certificate.PairSemantics.raw5260step0 line 240
  50. def OAI.MUB6.Certificate.PairSemantics.raw5260step1 line 242
  51. def OAI.MUB6.Certificate.PairSemantics.raw5260step2 line 244
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical5260 line 246
  53. def OAI.MUB6.Certificate.PairSemantics.raw5261 line 263
  54. def OAI.MUB6.Certificate.PairSemantics.raw5261step0 line 265
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5261 line 267
  56. def OAI.MUB6.Certificate.PairSemantics.raw5262 line 276
  57. def OAI.MUB6.Certificate.PairSemantics.raw5262step0 line 278
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical5262 line 280
  59. def OAI.MUB6.Certificate.PairSemantics.raw5263 line 289
  60. def OAI.MUB6.Certificate.PairSemantics.raw5263step0 line 291
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical5263 line 293
  62. def OAI.MUB6.Certificate.PairSemantics.raw5264 line 302
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical5264 line 304
  64. def OAI.MUB6.Certificate.PairSemantics.raw5265 line 308
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical5265 line 310
  66. def OAI.MUB6.Certificate.PairSemantics.raw5266 line 314
  67. def OAI.MUB6.Certificate.PairSemantics.raw5266step0 line 316
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical5266 line 318
  69. def OAI.MUB6.Certificate.PairSemantics.raw5267 line 327
  70. def OAI.MUB6.Certificate.PairSemantics.raw5267step0 line 329
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical5267 line 331
  72. def OAI.MUB6.Certificate.PairSemantics.raw5268 line 340
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical5268 line 342
  74. def OAI.MUB6.Certificate.PairSemantics.raw5269 line 346
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical5269 line 348
  76. def OAI.MUB6.Certificate.PairSemantics.raw5270 line 352
  77. def OAI.MUB6.Certificate.PairSemantics.raw5270step0 line 354
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical5270 line 356
  79. def OAI.MUB6.Certificate.PairSemantics.raw5271 line 365
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical5271 line 367
  81. def OAI.MUB6.Certificate.PairSemantics.raw5272 line 371
  82. def OAI.MUB6.Certificate.PairSemantics.raw5272step0 line 373
  83. def OAI.MUB6.Certificate.PairSemantics.raw5272step1 line 375
  84. def OAI.MUB6.Certificate.PairSemantics.raw5272step2 line 377
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical5272 line 379
  86. def OAI.MUB6.Certificate.PairSemantics.raw5273 line 396
  87. def OAI.MUB6.Certificate.PairSemantics.raw5273step0 line 398
  88. def OAI.MUB6.Certificate.PairSemantics.raw5273step1 line 400
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5273 line 402
  90. def OAI.MUB6.Certificate.PairSemantics.raw5274 line 415
  91. def OAI.MUB6.Certificate.PairSemantics.raw5274step0 line 417
  92. def OAI.MUB6.Certificate.PairSemantics.raw5274step1 line 419
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5274 line 421
  94. def OAI.MUB6.Certificate.PairSemantics.raw5275 line 434
  95. def OAI.MUB6.Certificate.PairSemantics.raw5275step0 line 436
  96. def OAI.MUB6.Certificate.PairSemantics.raw5275step1 line 438
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical5275 line 440
  98. def OAI.MUB6.Certificate.PairSemantics.raw5276 line 453
  99. def OAI.MUB6.Certificate.PairSemantics.raw5276step0 line 455
  100. def OAI.MUB6.Certificate.PairSemantics.raw5276step1 line 457
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical5276 line 459
  102. def OAI.MUB6.Certificate.PairSemantics.raw5277 line 472
  103. def OAI.MUB6.Certificate.PairSemantics.raw5277step0 line 474
  104. def OAI.MUB6.Certificate.PairSemantics.raw5277step1 line 476
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical5277 line 478
  106. def OAI.MUB6.Certificate.PairSemantics.raw5278 line 491
  107. def OAI.MUB6.Certificate.PairSemantics.raw5278step0 line 493
  108. def OAI.MUB6.Certificate.PairSemantics.raw5278step1 line 495
  109. def OAI.MUB6.Certificate.PairSemantics.raw5278step2 line 497
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical5278 line 499
  111. def OAI.MUB6.Certificate.PairSemantics.raw5279 line 517
  112. def OAI.MUB6.Certificate.PairSemantics.raw5279step0 line 519
  113. def OAI.MUB6.Certificate.PairSemantics.raw5279step1 line 521
  114. def OAI.MUB6.Certificate.PairSemantics.raw5279step2 line 523
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical5279 line 525