OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical290.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9280 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw9280step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw9280step1 line 25
  4. def OAI.MUB6.Certificate.PairSemantics.raw9280step2 line 27
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical9280 line 29
  6. def OAI.MUB6.Certificate.PairSemantics.raw9281 line 47
  7. def OAI.MUB6.Certificate.PairSemantics.raw9281step0 line 49
  8. def OAI.MUB6.Certificate.PairSemantics.raw9281step1 line 51
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9281 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw9282 line 67
  11. def OAI.MUB6.Certificate.PairSemantics.raw9282step0 line 69
  12. def OAI.MUB6.Certificate.PairSemantics.raw9282step1 line 71
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical9282 line 73
  14. def OAI.MUB6.Certificate.PairSemantics.raw9283 line 87
  15. def OAI.MUB6.Certificate.PairSemantics.raw9283step0 line 89
  16. def OAI.MUB6.Certificate.PairSemantics.raw9283step1 line 91
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical9283 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw9284 line 107
  19. def OAI.MUB6.Certificate.PairSemantics.raw9284step0 line 109
  20. def OAI.MUB6.Certificate.PairSemantics.raw9284step1 line 111
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical9284 line 113
  22. def OAI.MUB6.Certificate.PairSemantics.raw9285 line 127
  23. def OAI.MUB6.Certificate.PairSemantics.raw9285step0 line 129
  24. def OAI.MUB6.Certificate.PairSemantics.raw9285step1 line 131
  25. def OAI.MUB6.Certificate.PairSemantics.raw9285step2 line 133
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical9285 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw9286 line 153
  28. def OAI.MUB6.Certificate.PairSemantics.raw9286step0 line 155
  29. def OAI.MUB6.Certificate.PairSemantics.raw9286step1 line 157
  30. def OAI.MUB6.Certificate.PairSemantics.raw9286step2 line 159
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical9286 line 161
  32. def OAI.MUB6.Certificate.PairSemantics.raw9287 line 179
  33. def OAI.MUB6.Certificate.PairSemantics.raw9287step0 line 181
  34. def OAI.MUB6.Certificate.PairSemantics.raw9287step1 line 183
  35. def OAI.MUB6.Certificate.PairSemantics.raw9287step2 line 185
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical9287 line 187
  37. def OAI.MUB6.Certificate.PairSemantics.raw9288 line 205
  38. def OAI.MUB6.Certificate.PairSemantics.raw9288step0 line 207
  39. def OAI.MUB6.Certificate.PairSemantics.raw9288step1 line 209
  40. def OAI.MUB6.Certificate.PairSemantics.raw9288step2 line 211
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9288 line 213
  42. def OAI.MUB6.Certificate.PairSemantics.raw9289 line 231
  43. def OAI.MUB6.Certificate.PairSemantics.raw9289step0 line 233
  44. def OAI.MUB6.Certificate.PairSemantics.raw9289step1 line 235
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical9289 line 237
  46. def OAI.MUB6.Certificate.PairSemantics.raw9290 line 251
  47. def OAI.MUB6.Certificate.PairSemantics.raw9290step0 line 253
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical9290 line 255
  49. def OAI.MUB6.Certificate.PairSemantics.raw9291 line 264
  50. def OAI.MUB6.Certificate.PairSemantics.raw9291step0 line 266
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical9291 line 268
  52. def OAI.MUB6.Certificate.PairSemantics.raw9292 line 277
  53. def OAI.MUB6.Certificate.PairSemantics.raw9292step0 line 279
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical9292 line 281
  55. def OAI.MUB6.Certificate.PairSemantics.raw9293 line 290
  56. def OAI.MUB6.Certificate.PairSemantics.raw9293step0 line 292
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical9293 line 294
  58. def OAI.MUB6.Certificate.PairSemantics.raw9294 line 303
  59. def OAI.MUB6.Certificate.PairSemantics.raw9294step0 line 305
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical9294 line 307
  61. def OAI.MUB6.Certificate.PairSemantics.raw9295 line 316
  62. def OAI.MUB6.Certificate.PairSemantics.raw9295step0 line 318
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical9295 line 320
  64. def OAI.MUB6.Certificate.PairSemantics.raw9296 line 329
  65. def OAI.MUB6.Certificate.PairSemantics.raw9296step0 line 331
  66. def OAI.MUB6.Certificate.PairSemantics.raw9296step1 line 333
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical9296 line 335
  68. def OAI.MUB6.Certificate.PairSemantics.raw9297 line 348
  69. def OAI.MUB6.Certificate.PairSemantics.raw9297step0 line 350
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical9297 line 352
  71. def OAI.MUB6.Certificate.PairSemantics.raw9298 line 361
  72. def OAI.MUB6.Certificate.PairSemantics.raw9298step0 line 363
  73. def OAI.MUB6.Certificate.PairSemantics.raw9298step1 line 365
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical9298 line 367
  75. def OAI.MUB6.Certificate.PairSemantics.raw9299 line 380
  76. def OAI.MUB6.Certificate.PairSemantics.raw9299step0 line 382
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical9299 line 384
  78. def OAI.MUB6.Certificate.PairSemantics.raw9300 line 393
  79. def OAI.MUB6.Certificate.PairSemantics.raw9300step0 line 395
  80. def OAI.MUB6.Certificate.PairSemantics.raw9300step1 line 397
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical9300 line 399
  82. def OAI.MUB6.Certificate.PairSemantics.raw9301 line 412
  83. def OAI.MUB6.Certificate.PairSemantics.raw9301step0 line 414
  84. def OAI.MUB6.Certificate.PairSemantics.raw9301step1 line 416
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical9301 line 418
  86. def OAI.MUB6.Certificate.PairSemantics.raw9302 line 431
  87. def OAI.MUB6.Certificate.PairSemantics.raw9302step0 line 433
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical9302 line 435
  89. def OAI.MUB6.Certificate.PairSemantics.raw9303 line 444
  90. def OAI.MUB6.Certificate.PairSemantics.raw9303step0 line 446
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical9303 line 448
  92. def OAI.MUB6.Certificate.PairSemantics.raw9304 line 457
  93. def OAI.MUB6.Certificate.PairSemantics.raw9304step0 line 459
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical9304 line 461
  95. def OAI.MUB6.Certificate.PairSemantics.raw9305 line 470
  96. def OAI.MUB6.Certificate.PairSemantics.raw9305step0 line 472
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical9305 line 474
  98. def OAI.MUB6.Certificate.PairSemantics.raw9306 line 483
  99. def OAI.MUB6.Certificate.PairSemantics.raw9306step0 line 485
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical9306 line 487
  101. def OAI.MUB6.Certificate.PairSemantics.raw9307 line 496
  102. def OAI.MUB6.Certificate.PairSemantics.raw9307step0 line 498
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical9307 line 500
  104. def OAI.MUB6.Certificate.PairSemantics.raw9308 line 509
  105. def OAI.MUB6.Certificate.PairSemantics.raw9308step0 line 511
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical9308 line 513
  107. def OAI.MUB6.Certificate.PairSemantics.raw9309 line 522
  108. def OAI.MUB6.Certificate.PairSemantics.raw9309step0 line 524
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical9309 line 526
  110. def OAI.MUB6.Certificate.PairSemantics.raw9310 line 535
  111. def OAI.MUB6.Certificate.PairSemantics.raw9310step0 line 537
  112. def OAI.MUB6.Certificate.PairSemantics.raw9310step1 line 539
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical9310 line 541
  114. def OAI.MUB6.Certificate.PairSemantics.raw9311 line 554
  115. def OAI.MUB6.Certificate.PairSemantics.raw9311step0 line 556
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical9311 line 558