OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical77.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2464 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw2464step0 line 17
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical2464 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw2465 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw2465step0 line 30
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical2465 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw2466 line 41
  8. def OAI.MUB6.Certificate.PairSemantics.raw2466step0 line 43
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical2466 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw2467 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw2467step0 line 56
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2467 line 58
  13. def OAI.MUB6.Certificate.PairSemantics.raw2468 line 67
  14. def OAI.MUB6.Certificate.PairSemantics.raw2468step0 line 69
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical2468 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw2469 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw2469step0 line 82
  18. def OAI.MUB6.Certificate.PairSemantics.raw2469step1 line 84
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical2469 line 86
  20. def OAI.MUB6.Certificate.PairSemantics.raw2470 line 99
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical2470 line 101
  22. def OAI.MUB6.Certificate.PairSemantics.raw2471 line 105
  23. def OAI.MUB6.Certificate.PairSemantics.raw2471step0 line 107
  24. def OAI.MUB6.Certificate.PairSemantics.raw2471step1 line 109
  25. def OAI.MUB6.Certificate.PairSemantics.raw2471step2 line 111
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical2471 line 113
  27. def OAI.MUB6.Certificate.PairSemantics.raw2472 line 130
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2472 line 132
  29. def OAI.MUB6.Certificate.PairSemantics.raw2473 line 136
  30. def OAI.MUB6.Certificate.PairSemantics.raw2473step0 line 138
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2473 line 140
  32. def OAI.MUB6.Certificate.PairSemantics.raw2474 line 149
  33. def OAI.MUB6.Certificate.PairSemantics.raw2474step0 line 151
  34. def OAI.MUB6.Certificate.PairSemantics.raw2474step1 line 153
  35. def OAI.MUB6.Certificate.PairSemantics.raw2474step2 line 155
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2474 line 157
  37. def OAI.MUB6.Certificate.PairSemantics.raw2475 line 174
  38. def OAI.MUB6.Certificate.PairSemantics.raw2475step0 line 176
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2475 line 178
  40. def OAI.MUB6.Certificate.PairSemantics.raw2476 line 187
  41. def OAI.MUB6.Certificate.PairSemantics.raw2476step0 line 189
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2476 line 191
  43. def OAI.MUB6.Certificate.PairSemantics.raw2477 line 200
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical2477 line 202
  45. def OAI.MUB6.Certificate.PairSemantics.raw2478 line 206
  46. def OAI.MUB6.Certificate.PairSemantics.raw2478step0 line 208
  47. def OAI.MUB6.Certificate.PairSemantics.raw2478step1 line 210
  48. def OAI.MUB6.Certificate.PairSemantics.raw2478step2 line 212
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2478 line 214
  50. def OAI.MUB6.Certificate.PairSemantics.raw2479 line 231
  51. def OAI.MUB6.Certificate.PairSemantics.raw2479step0 line 233
  52. def OAI.MUB6.Certificate.PairSemantics.raw2479step1 line 235
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical2479 line 237
  54. def OAI.MUB6.Certificate.PairSemantics.raw2480 line 250
  55. def OAI.MUB6.Certificate.PairSemantics.raw2480step0 line 252
  56. def OAI.MUB6.Certificate.PairSemantics.raw2480step1 line 254
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2480 line 256
  58. def OAI.MUB6.Certificate.PairSemantics.raw2481 line 269
  59. def OAI.MUB6.Certificate.PairSemantics.raw2481step0 line 271
  60. def OAI.MUB6.Certificate.PairSemantics.raw2481step1 line 273
  61. def OAI.MUB6.Certificate.PairSemantics.raw2481step2 line 275
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical2481 line 277
  63. def OAI.MUB6.Certificate.PairSemantics.raw2482 line 294
  64. def OAI.MUB6.Certificate.PairSemantics.raw2482step0 line 296
  65. def OAI.MUB6.Certificate.PairSemantics.raw2482step1 line 298
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2482 line 300
  67. def OAI.MUB6.Certificate.PairSemantics.raw2483 line 313
  68. def OAI.MUB6.Certificate.PairSemantics.raw2483step0 line 315
  69. def OAI.MUB6.Certificate.PairSemantics.raw2483step1 line 317
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical2483 line 319
  71. def OAI.MUB6.Certificate.PairSemantics.raw2484 line 332
  72. def OAI.MUB6.Certificate.PairSemantics.raw2484step0 line 334
  73. def OAI.MUB6.Certificate.PairSemantics.raw2484step1 line 336
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical2484 line 338
  75. def OAI.MUB6.Certificate.PairSemantics.raw2485 line 351
  76. def OAI.MUB6.Certificate.PairSemantics.raw2485step0 line 353
  77. def OAI.MUB6.Certificate.PairSemantics.raw2485step1 line 355
  78. def OAI.MUB6.Certificate.PairSemantics.raw2485step2 line 357
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2485 line 359
  80. def OAI.MUB6.Certificate.PairSemantics.raw2486 line 376
  81. def OAI.MUB6.Certificate.PairSemantics.raw2486step0 line 378
  82. def OAI.MUB6.Certificate.PairSemantics.raw2486step1 line 380
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2486 line 382
  84. def OAI.MUB6.Certificate.PairSemantics.raw2487 line 395
  85. def OAI.MUB6.Certificate.PairSemantics.raw2487step0 line 397
  86. def OAI.MUB6.Certificate.PairSemantics.raw2487step1 line 399
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical2487 line 401
  88. def OAI.MUB6.Certificate.PairSemantics.raw2488 line 414
  89. def OAI.MUB6.Certificate.PairSemantics.raw2488step0 line 416
  90. def OAI.MUB6.Certificate.PairSemantics.raw2488step1 line 418
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical2488 line 420
  92. def OAI.MUB6.Certificate.PairSemantics.raw2489 line 433
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical2489 line 435
  94. def OAI.MUB6.Certificate.PairSemantics.raw2490 line 439
  95. def OAI.MUB6.Certificate.PairSemantics.raw2490step0 line 441
  96. def OAI.MUB6.Certificate.PairSemantics.raw2490step1 line 443
  97. def OAI.MUB6.Certificate.PairSemantics.raw2490step2 line 445
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical2490 line 447
  99. def OAI.MUB6.Certificate.PairSemantics.raw2491 line 464
  100. def OAI.MUB6.Certificate.PairSemantics.raw2491step0 line 466
  101. def OAI.MUB6.Certificate.PairSemantics.raw2491step1 line 468
  102. def OAI.MUB6.Certificate.PairSemantics.raw2491step2 line 470
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical2491 line 472
  104. def OAI.MUB6.Certificate.PairSemantics.raw2492 line 489
  105. def OAI.MUB6.Certificate.PairSemantics.raw2492step0 line 491
  106. def OAI.MUB6.Certificate.PairSemantics.raw2492step1 line 493
  107. def OAI.MUB6.Certificate.PairSemantics.raw2492step2 line 495
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical2492 line 497
  109. def OAI.MUB6.Certificate.PairSemantics.raw2493 line 514
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical2493 line 516
  111. def OAI.MUB6.Certificate.PairSemantics.raw2494 line 520
  112. def OAI.MUB6.Certificate.PairSemantics.raw2494step0 line 522
  113. def OAI.MUB6.Certificate.PairSemantics.raw2494step1 line 524
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical2494 line 526
  115. def OAI.MUB6.Certificate.PairSemantics.raw2495 line 539
  116. def OAI.MUB6.Certificate.PairSemantics.raw2495step0 line 541
  117. def OAI.MUB6.Certificate.PairSemantics.raw2495step1 line 543
  118. def OAI.MUB6.Certificate.PairSemantics.raw2495step2 line 545
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical2495 line 547