OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical106.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3392 line 19
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical3392 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw3393 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3393 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw3394 line 31
  6. def OAI.MUB6.Certificate.PairSemantics.raw3394step0 line 33
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3394 line 35
  8. def OAI.MUB6.Certificate.PairSemantics.raw3395 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw3395step0 line 46
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical3395 line 48
  11. def OAI.MUB6.Certificate.PairSemantics.raw3396 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw3396step0 line 59
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical3396 line 61
  14. def OAI.MUB6.Certificate.PairSemantics.raw3397 line 70
  15. def OAI.MUB6.Certificate.PairSemantics.raw3397step0 line 72
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3397 line 74
  17. def OAI.MUB6.Certificate.PairSemantics.raw3398 line 83
  18. def OAI.MUB6.Certificate.PairSemantics.raw3398step0 line 85
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical3398 line 87
  20. def OAI.MUB6.Certificate.PairSemantics.raw3399 line 96
  21. def OAI.MUB6.Certificate.PairSemantics.raw3399step0 line 98
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical3399 line 100
  23. def OAI.MUB6.Certificate.PairSemantics.raw3400 line 109
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3400 line 111
  25. def OAI.MUB6.Certificate.PairSemantics.raw3401 line 115
  26. def OAI.MUB6.Certificate.PairSemantics.raw3401step0 line 117
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical3401 line 119
  28. def OAI.MUB6.Certificate.PairSemantics.raw3402 line 128
  29. def OAI.MUB6.Certificate.PairSemantics.raw3402step0 line 130
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical3402 line 132
  31. def OAI.MUB6.Certificate.PairSemantics.raw3403 line 141
  32. def OAI.MUB6.Certificate.PairSemantics.raw3403step0 line 143
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical3403 line 145
  34. def OAI.MUB6.Certificate.PairSemantics.raw3404 line 154
  35. def OAI.MUB6.Certificate.PairSemantics.raw3404step0 line 156
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical3404 line 158
  37. def OAI.MUB6.Certificate.PairSemantics.raw3405 line 167
  38. def OAI.MUB6.Certificate.PairSemantics.raw3405step0 line 169
  39. def OAI.MUB6.Certificate.PairSemantics.raw3405step1 line 171
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical3405 line 173
  41. def OAI.MUB6.Certificate.PairSemantics.raw3406 line 186
  42. def OAI.MUB6.Certificate.PairSemantics.raw3406step0 line 188
  43. def OAI.MUB6.Certificate.PairSemantics.raw3406step1 line 190
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical3406 line 192
  45. def OAI.MUB6.Certificate.PairSemantics.raw3407 line 205
  46. def OAI.MUB6.Certificate.PairSemantics.raw3407step0 line 207
  47. def OAI.MUB6.Certificate.PairSemantics.raw3407step1 line 209
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical3407 line 211
  49. def OAI.MUB6.Certificate.PairSemantics.raw3408 line 224
  50. def OAI.MUB6.Certificate.PairSemantics.raw3408step0 line 226
  51. def OAI.MUB6.Certificate.PairSemantics.raw3408step1 line 228
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical3408 line 230
  53. def OAI.MUB6.Certificate.PairSemantics.raw3409 line 243
  54. def OAI.MUB6.Certificate.PairSemantics.raw3409step0 line 245
  55. def OAI.MUB6.Certificate.PairSemantics.raw3409step1 line 247
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical3409 line 249
  57. def OAI.MUB6.Certificate.PairSemantics.raw3410 line 262
  58. def OAI.MUB6.Certificate.PairSemantics.raw3410step0 line 264
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical3410 line 266
  60. def OAI.MUB6.Certificate.PairSemantics.raw3411 line 275
  61. def OAI.MUB6.Certificate.PairSemantics.raw3411step0 line 277
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical3411 line 279
  63. def OAI.MUB6.Certificate.PairSemantics.raw3412 line 288
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical3412 line 290
  65. def OAI.MUB6.Certificate.PairSemantics.raw3413 line 294
  66. def OAI.MUB6.Certificate.PairSemantics.raw3413step0 line 296
  67. def OAI.MUB6.Certificate.PairSemantics.raw3413step1 line 298
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical3413 line 300
  69. def OAI.MUB6.Certificate.PairSemantics.raw3414 line 313
  70. def OAI.MUB6.Certificate.PairSemantics.raw3414step0 line 315
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical3414 line 317
  72. def OAI.MUB6.Certificate.PairSemantics.raw3415 line 326
  73. def OAI.MUB6.Certificate.PairSemantics.raw3415step0 line 328
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical3415 line 330
  75. def OAI.MUB6.Certificate.PairSemantics.raw3416 line 339
  76. def OAI.MUB6.Certificate.PairSemantics.raw3416step0 line 341
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical3416 line 343
  78. def OAI.MUB6.Certificate.PairSemantics.raw3417 line 352
  79. def OAI.MUB6.Certificate.PairSemantics.raw3417step0 line 354
  80. def OAI.MUB6.Certificate.PairSemantics.raw3417step1 line 356
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical3417 line 358
  82. def OAI.MUB6.Certificate.PairSemantics.raw3418 line 371
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical3418 line 373
  84. def OAI.MUB6.Certificate.PairSemantics.raw3419 line 377
  85. def OAI.MUB6.Certificate.PairSemantics.raw3419step0 line 379
  86. def OAI.MUB6.Certificate.PairSemantics.raw3419step1 line 381
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical3419 line 383
  88. def OAI.MUB6.Certificate.PairSemantics.raw3420 line 396
  89. def OAI.MUB6.Certificate.PairSemantics.raw3420step0 line 398
  90. def OAI.MUB6.Certificate.PairSemantics.raw3420step1 line 400
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical3420 line 402
  92. def OAI.MUB6.Certificate.PairSemantics.raw3421 line 415
  93. def OAI.MUB6.Certificate.PairSemantics.raw3421step0 line 417
  94. def OAI.MUB6.Certificate.PairSemantics.raw3421step1 line 419
  95. def OAI.MUB6.Certificate.PairSemantics.raw3421step2 line 421
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical3421 line 423
  97. def OAI.MUB6.Certificate.PairSemantics.raw3422 line 440
  98. def OAI.MUB6.Certificate.PairSemantics.raw3422step0 line 442
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical3422 line 444
  100. def OAI.MUB6.Certificate.PairSemantics.raw3423 line 453
  101. def OAI.MUB6.Certificate.PairSemantics.raw3423step0 line 455
  102. def OAI.MUB6.Certificate.PairSemantics.raw3423step1 line 457
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical3423 line 459