OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical133.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4256 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical4256 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw4257 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4257 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw4258 line 28
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical4258 line 30
  7. def OAI.MUB6.Certificate.PairSemantics.raw4259 line 34
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical4259 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw4260 line 40
  10. def OAI.MUB6.Certificate.PairSemantics.raw4260step0 line 42
  11. def OAI.MUB6.Certificate.PairSemantics.raw4260step1 line 44
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical4260 line 46
  13. def OAI.MUB6.Certificate.PairSemantics.raw4261 line 59
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4261 line 61
  15. def OAI.MUB6.Certificate.PairSemantics.raw4262 line 65
  16. def OAI.MUB6.Certificate.PairSemantics.raw4262step0 line 67
  17. def OAI.MUB6.Certificate.PairSemantics.raw4262step1 line 69
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical4262 line 71
  19. def OAI.MUB6.Certificate.PairSemantics.raw4263 line 84
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4263 line 86
  21. def OAI.MUB6.Certificate.PairSemantics.raw4264 line 90
  22. def OAI.MUB6.Certificate.PairSemantics.raw4264step0 line 92
  23. def OAI.MUB6.Certificate.PairSemantics.raw4264step1 line 94
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical4264 line 96
  25. def OAI.MUB6.Certificate.PairSemantics.raw4265 line 109
  26. def OAI.MUB6.Certificate.PairSemantics.raw4265step0 line 111
  27. def OAI.MUB6.Certificate.PairSemantics.raw4265step1 line 113
  28. def OAI.MUB6.Certificate.PairSemantics.raw4265step2 line 115
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical4265 line 117
  30. def OAI.MUB6.Certificate.PairSemantics.raw4266 line 134
  31. def OAI.MUB6.Certificate.PairSemantics.raw4266step0 line 136
  32. def OAI.MUB6.Certificate.PairSemantics.raw4266step1 line 138
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical4266 line 140
  34. def OAI.MUB6.Certificate.PairSemantics.raw4267 line 153
  35. def OAI.MUB6.Certificate.PairSemantics.raw4267step0 line 155
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical4267 line 157
  37. def OAI.MUB6.Certificate.PairSemantics.raw4268 line 166
  38. def OAI.MUB6.Certificate.PairSemantics.raw4268step0 line 168
  39. def OAI.MUB6.Certificate.PairSemantics.raw4268step1 line 170
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4268 line 172
  41. def OAI.MUB6.Certificate.PairSemantics.raw4269 line 185
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical4269 line 187
  43. def OAI.MUB6.Certificate.PairSemantics.raw4270 line 191
  44. def OAI.MUB6.Certificate.PairSemantics.raw4270step0 line 193
  45. def OAI.MUB6.Certificate.PairSemantics.raw4270step1 line 195
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical4270 line 197
  47. def OAI.MUB6.Certificate.PairSemantics.raw4271 line 210
  48. def OAI.MUB6.Certificate.PairSemantics.raw4271step0 line 212
  49. def OAI.MUB6.Certificate.PairSemantics.raw4271step1 line 214
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4271 line 216
  51. def OAI.MUB6.Certificate.PairSemantics.raw4272 line 229
  52. def OAI.MUB6.Certificate.PairSemantics.raw4272step0 line 231
  53. def OAI.MUB6.Certificate.PairSemantics.raw4272step1 line 233
  54. def OAI.MUB6.Certificate.PairSemantics.raw4272step2 line 235
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical4272 line 237
  56. def OAI.MUB6.Certificate.PairSemantics.raw4273 line 254
  57. def OAI.MUB6.Certificate.PairSemantics.raw4273step0 line 256
  58. def OAI.MUB6.Certificate.PairSemantics.raw4273step1 line 258
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical4273 line 260
  60. def OAI.MUB6.Certificate.PairSemantics.raw4274 line 273
  61. def OAI.MUB6.Certificate.PairSemantics.raw4274step0 line 275
  62. def OAI.MUB6.Certificate.PairSemantics.raw4274step1 line 277
  63. def OAI.MUB6.Certificate.PairSemantics.raw4274step2 line 279
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4274 line 281
  65. def OAI.MUB6.Certificate.PairSemantics.raw4275 line 298
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical4275 line 300
  67. def OAI.MUB6.Certificate.PairSemantics.raw4276 line 304
  68. def OAI.MUB6.Certificate.PairSemantics.raw4276step0 line 306
  69. def OAI.MUB6.Certificate.PairSemantics.raw4276step1 line 308
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4276 line 310
  71. def OAI.MUB6.Certificate.PairSemantics.raw4277 line 323
  72. def OAI.MUB6.Certificate.PairSemantics.raw4277step0 line 325
  73. def OAI.MUB6.Certificate.PairSemantics.raw4277step1 line 327
  74. def OAI.MUB6.Certificate.PairSemantics.raw4277step2 line 329
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical4277 line 331
  76. def OAI.MUB6.Certificate.PairSemantics.raw4278 line 348
  77. def OAI.MUB6.Certificate.PairSemantics.raw4278step0 line 350
  78. def OAI.MUB6.Certificate.PairSemantics.raw4278step1 line 352
  79. def OAI.MUB6.Certificate.PairSemantics.raw4278step2 line 354
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4278 line 356
  81. def OAI.MUB6.Certificate.PairSemantics.raw4279 line 373
  82. def OAI.MUB6.Certificate.PairSemantics.raw4279step0 line 375
  83. def OAI.MUB6.Certificate.PairSemantics.raw4279step1 line 377
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical4279 line 379
  85. def OAI.MUB6.Certificate.PairSemantics.raw4280 line 392
  86. def OAI.MUB6.Certificate.PairSemantics.raw4280step0 line 394
  87. def OAI.MUB6.Certificate.PairSemantics.raw4280step1 line 396
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical4280 line 398
  89. def OAI.MUB6.Certificate.PairSemantics.raw4281 line 411
  90. def OAI.MUB6.Certificate.PairSemantics.raw4281step0 line 413
  91. def OAI.MUB6.Certificate.PairSemantics.raw4281step1 line 415
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical4281 line 417
  93. def OAI.MUB6.Certificate.PairSemantics.raw4282 line 430
  94. def OAI.MUB6.Certificate.PairSemantics.raw4282step0 line 432
  95. def OAI.MUB6.Certificate.PairSemantics.raw4282step1 line 434
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical4282 line 436
  97. def OAI.MUB6.Certificate.PairSemantics.raw4283 line 449
  98. def OAI.MUB6.Certificate.PairSemantics.raw4283step0 line 451
  99. def OAI.MUB6.Certificate.PairSemantics.raw4283step1 line 453
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical4283 line 455
  101. def OAI.MUB6.Certificate.PairSemantics.raw4284 line 468
  102. def OAI.MUB6.Certificate.PairSemantics.raw4284step0 line 470
  103. def OAI.MUB6.Certificate.PairSemantics.raw4284step1 line 472
  104. def OAI.MUB6.Certificate.PairSemantics.raw4284step2 line 474
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical4284 line 476
  106. def OAI.MUB6.Certificate.PairSemantics.raw4285 line 493
  107. def OAI.MUB6.Certificate.PairSemantics.raw4285step0 line 495
  108. def OAI.MUB6.Certificate.PairSemantics.raw4285step1 line 497
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical4285 line 499
  110. def OAI.MUB6.Certificate.PairSemantics.raw4286 line 512
  111. def OAI.MUB6.Certificate.PairSemantics.raw4286step0 line 514
  112. def OAI.MUB6.Certificate.PairSemantics.raw4286step1 line 516
  113. def OAI.MUB6.Certificate.PairSemantics.raw4286step2 line 518
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical4286 line 520
  115. def OAI.MUB6.Certificate.PairSemantics.raw4287 line 537
  116. def OAI.MUB6.Certificate.PairSemantics.raw4287step0 line 539
  117. def OAI.MUB6.Certificate.PairSemantics.raw4287step1 line 541
  118. def OAI.MUB6.Certificate.PairSemantics.raw4287step2 line 543
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical4287 line 545