OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical163.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5216 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw5216step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw5216step1 line 25
  4. def OAI.MUB6.Certificate.PairSemantics.raw5216step2 line 27
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical5216 line 29
  6. def OAI.MUB6.Certificate.PairSemantics.raw5217 line 49
  7. def OAI.MUB6.Certificate.PairSemantics.raw5217step0 line 51
  8. def OAI.MUB6.Certificate.PairSemantics.raw5217step1 line 53
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical5217 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw5218 line 69
  11. def OAI.MUB6.Certificate.PairSemantics.raw5218step0 line 71
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical5218 line 73
  13. def OAI.MUB6.Certificate.PairSemantics.raw5219 line 82
  14. def OAI.MUB6.Certificate.PairSemantics.raw5219step0 line 84
  15. def OAI.MUB6.Certificate.PairSemantics.raw5219step1 line 86
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical5219 line 88
  17. def OAI.MUB6.Certificate.PairSemantics.raw5220 line 101
  18. def OAI.MUB6.Certificate.PairSemantics.raw5220step0 line 103
  19. def OAI.MUB6.Certificate.PairSemantics.raw5220step1 line 105
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical5220 line 107
  21. def OAI.MUB6.Certificate.PairSemantics.raw5221 line 120
  22. def OAI.MUB6.Certificate.PairSemantics.raw5221step0 line 122
  23. def OAI.MUB6.Certificate.PairSemantics.raw5221step1 line 124
  24. def OAI.MUB6.Certificate.PairSemantics.raw5221step2 line 126
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical5221 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw5222 line 145
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical5222 line 147
  28. def OAI.MUB6.Certificate.PairSemantics.raw5223 line 151
  29. def OAI.MUB6.Certificate.PairSemantics.raw5223step0 line 153
  30. def OAI.MUB6.Certificate.PairSemantics.raw5223step1 line 155
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical5223 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw5224 line 170
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical5224 line 172
  34. def OAI.MUB6.Certificate.PairSemantics.raw5225 line 176
  35. def OAI.MUB6.Certificate.PairSemantics.raw5225step0 line 178
  36. def OAI.MUB6.Certificate.PairSemantics.raw5225step1 line 180
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical5225 line 182
  38. def OAI.MUB6.Certificate.PairSemantics.raw5226 line 195
  39. def OAI.MUB6.Certificate.PairSemantics.raw5226step0 line 197
  40. def OAI.MUB6.Certificate.PairSemantics.raw5226step1 line 199
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical5226 line 201
  42. def OAI.MUB6.Certificate.PairSemantics.raw5227 line 214
  43. def OAI.MUB6.Certificate.PairSemantics.raw5227step0 line 216
  44. def OAI.MUB6.Certificate.PairSemantics.raw5227step1 line 218
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical5227 line 220
  46. def OAI.MUB6.Certificate.PairSemantics.raw5228 line 233
  47. def OAI.MUB6.Certificate.PairSemantics.raw5228step0 line 235
  48. def OAI.MUB6.Certificate.PairSemantics.raw5228step1 line 237
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical5228 line 239
  50. def OAI.MUB6.Certificate.PairSemantics.raw5229 line 252
  51. def OAI.MUB6.Certificate.PairSemantics.raw5229step0 line 254
  52. def OAI.MUB6.Certificate.PairSemantics.raw5229step1 line 256
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical5229 line 258
  54. def OAI.MUB6.Certificate.PairSemantics.raw5230 line 271
  55. def OAI.MUB6.Certificate.PairSemantics.raw5230step0 line 273
  56. def OAI.MUB6.Certificate.PairSemantics.raw5230step1 line 275
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical5230 line 277
  58. def OAI.MUB6.Certificate.PairSemantics.raw5231 line 290
  59. def OAI.MUB6.Certificate.PairSemantics.raw5231step0 line 292
  60. def OAI.MUB6.Certificate.PairSemantics.raw5231step1 line 294
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical5231 line 296
  62. def OAI.MUB6.Certificate.PairSemantics.raw5232 line 309
  63. def OAI.MUB6.Certificate.PairSemantics.raw5232step0 line 311
  64. def OAI.MUB6.Certificate.PairSemantics.raw5232step1 line 313
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical5232 line 315
  66. def OAI.MUB6.Certificate.PairSemantics.raw5233 line 328
  67. def OAI.MUB6.Certificate.PairSemantics.raw5233step0 line 330
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical5233 line 332
  69. def OAI.MUB6.Certificate.PairSemantics.raw5234 line 341
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical5234 line 343
  71. def OAI.MUB6.Certificate.PairSemantics.raw5235 line 347
  72. def OAI.MUB6.Certificate.PairSemantics.raw5235step0 line 349
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical5235 line 351
  74. def OAI.MUB6.Certificate.PairSemantics.raw5236 line 360
  75. def OAI.MUB6.Certificate.PairSemantics.raw5236step0 line 362
  76. def OAI.MUB6.Certificate.PairSemantics.raw5236step1 line 364
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical5236 line 366
  78. def OAI.MUB6.Certificate.PairSemantics.raw5237 line 379
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5237 line 381
  80. def OAI.MUB6.Certificate.PairSemantics.raw5238 line 385
  81. def OAI.MUB6.Certificate.PairSemantics.raw5238step0 line 387
  82. def OAI.MUB6.Certificate.PairSemantics.raw5238step1 line 389
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical5238 line 391
  84. def OAI.MUB6.Certificate.PairSemantics.raw5239 line 404
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical5239 line 406
  86. def OAI.MUB6.Certificate.PairSemantics.raw5240 line 410
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical5240 line 412
  88. def OAI.MUB6.Certificate.PairSemantics.raw5241 line 416
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5241 line 418
  90. def OAI.MUB6.Certificate.PairSemantics.raw5242 line 422
  91. def OAI.MUB6.Certificate.PairSemantics.raw5242step0 line 424
  92. def OAI.MUB6.Certificate.PairSemantics.raw5242step1 line 426
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5242 line 428
  94. def OAI.MUB6.Certificate.PairSemantics.raw5243 line 441
  95. def OAI.MUB6.Certificate.PairSemantics.raw5243step0 line 443
  96. def OAI.MUB6.Certificate.PairSemantics.raw5243step1 line 445
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical5243 line 447
  98. def OAI.MUB6.Certificate.PairSemantics.raw5244 line 460
  99. def OAI.MUB6.Certificate.PairSemantics.raw5244step0 line 462
  100. def OAI.MUB6.Certificate.PairSemantics.raw5244step1 line 464
  101. def OAI.MUB6.Certificate.PairSemantics.raw5244step2 line 466
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical5244 line 468
  103. def OAI.MUB6.Certificate.PairSemantics.raw5245 line 485
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical5245 line 487
  105. def OAI.MUB6.Certificate.PairSemantics.raw5246 line 491
  106. def OAI.MUB6.Certificate.PairSemantics.raw5246step0 line 493
  107. def OAI.MUB6.Certificate.PairSemantics.raw5246step1 line 495
  108. def OAI.MUB6.Certificate.PairSemantics.raw5246step2 line 497
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical5246 line 499
  110. def OAI.MUB6.Certificate.PairSemantics.raw5247 line 516
  111. def OAI.MUB6.Certificate.PairSemantics.raw5247step0 line 518
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical5247 line 520