OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical109.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3488 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw3488step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical3488 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw3489 line 31
  5. def OAI.MUB6.Certificate.PairSemantics.raw3489step0 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw3489step1 line 35
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3489 line 37
  8. def OAI.MUB6.Certificate.PairSemantics.raw3490 line 50
  9. def OAI.MUB6.Certificate.PairSemantics.raw3490step0 line 52
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical3490 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw3491 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw3491step0 line 65
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical3491 line 67
  14. def OAI.MUB6.Certificate.PairSemantics.raw3492 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw3492step0 line 78
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3492 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw3493 line 89
  18. def OAI.MUB6.Certificate.PairSemantics.raw3493step0 line 91
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical3493 line 93
  20. def OAI.MUB6.Certificate.PairSemantics.raw3494 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw3494step0 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw3494step1 line 106
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical3494 line 108
  24. def OAI.MUB6.Certificate.PairSemantics.raw3495 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw3495step0 line 123
  26. def OAI.MUB6.Certificate.PairSemantics.raw3495step1 line 125
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical3495 line 127
  28. def OAI.MUB6.Certificate.PairSemantics.raw3496 line 140
  29. def OAI.MUB6.Certificate.PairSemantics.raw3496step0 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw3496step1 line 144
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical3496 line 146
  32. def OAI.MUB6.Certificate.PairSemantics.raw3497 line 159
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical3497 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw3498 line 165
  35. def OAI.MUB6.Certificate.PairSemantics.raw3498step0 line 167
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical3498 line 169
  37. def OAI.MUB6.Certificate.PairSemantics.raw3499 line 178
  38. def OAI.MUB6.Certificate.PairSemantics.raw3499step0 line 180
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3499 line 182
  40. def OAI.MUB6.Certificate.PairSemantics.raw3500 line 191
  41. def OAI.MUB6.Certificate.PairSemantics.raw3500step0 line 193
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical3500 line 195
  43. def OAI.MUB6.Certificate.PairSemantics.raw3501 line 204
  44. def OAI.MUB6.Certificate.PairSemantics.raw3501step0 line 206
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical3501 line 208
  46. def OAI.MUB6.Certificate.PairSemantics.raw3502 line 217
  47. def OAI.MUB6.Certificate.PairSemantics.raw3502step0 line 219
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical3502 line 221
  49. def OAI.MUB6.Certificate.PairSemantics.raw3503 line 230
  50. def OAI.MUB6.Certificate.PairSemantics.raw3503step0 line 232
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical3503 line 234
  52. def OAI.MUB6.Certificate.PairSemantics.raw3504 line 243
  53. def OAI.MUB6.Certificate.PairSemantics.raw3504step0 line 245
  54. def OAI.MUB6.Certificate.PairSemantics.raw3504step1 line 247
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3504 line 249
  56. def OAI.MUB6.Certificate.PairSemantics.raw3505 line 262
  57. def OAI.MUB6.Certificate.PairSemantics.raw3505step0 line 264
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical3505 line 266
  59. def OAI.MUB6.Certificate.PairSemantics.raw3506 line 275
  60. def OAI.MUB6.Certificate.PairSemantics.raw3506step0 line 277
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3506 line 279
  62. def OAI.MUB6.Certificate.PairSemantics.raw3507 line 288
  63. def OAI.MUB6.Certificate.PairSemantics.raw3507step0 line 290
  64. def OAI.MUB6.Certificate.PairSemantics.raw3507step1 line 292
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3507 line 294
  66. def OAI.MUB6.Certificate.PairSemantics.raw3508 line 307
  67. def OAI.MUB6.Certificate.PairSemantics.raw3508step0 line 309
  68. def OAI.MUB6.Certificate.PairSemantics.raw3508step1 line 311
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3508 line 313
  70. def OAI.MUB6.Certificate.PairSemantics.raw3509 line 326
  71. def OAI.MUB6.Certificate.PairSemantics.raw3509step0 line 328
  72. def OAI.MUB6.Certificate.PairSemantics.raw3509step1 line 330
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical3509 line 332
  74. def OAI.MUB6.Certificate.PairSemantics.raw3510 line 345
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3510 line 347
  76. def OAI.MUB6.Certificate.PairSemantics.raw3511 line 351
  77. def OAI.MUB6.Certificate.PairSemantics.raw3511step0 line 353
  78. def OAI.MUB6.Certificate.PairSemantics.raw3511step1 line 355
  79. def OAI.MUB6.Certificate.PairSemantics.raw3511step2 line 357
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical3511 line 359
  81. def OAI.MUB6.Certificate.PairSemantics.raw3512 line 376
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3512 line 378
  83. def OAI.MUB6.Certificate.PairSemantics.raw3513 line 382
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical3513 line 384
  85. def OAI.MUB6.Certificate.PairSemantics.raw3514 line 388
  86. def OAI.MUB6.Certificate.PairSemantics.raw3514step0 line 390
  87. def OAI.MUB6.Certificate.PairSemantics.raw3514step1 line 392
  88. def OAI.MUB6.Certificate.PairSemantics.raw3514step2 line 394
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3514 line 396
  90. def OAI.MUB6.Certificate.PairSemantics.raw3515 line 413
  91. def OAI.MUB6.Certificate.PairSemantics.raw3515step0 line 415
  92. def OAI.MUB6.Certificate.PairSemantics.raw3515step1 line 417
  93. def OAI.MUB6.Certificate.PairSemantics.raw3515step2 line 419
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical3515 line 421
  95. def OAI.MUB6.Certificate.PairSemantics.raw3516 line 438
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical3516 line 440
  97. def OAI.MUB6.Certificate.PairSemantics.raw3517 line 444
  98. def OAI.MUB6.Certificate.PairSemantics.raw3517step0 line 446
  99. def OAI.MUB6.Certificate.PairSemantics.raw3517step1 line 448
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3517 line 450
  101. def OAI.MUB6.Certificate.PairSemantics.raw3518 line 463
  102. def OAI.MUB6.Certificate.PairSemantics.raw3518step0 line 465
  103. def OAI.MUB6.Certificate.PairSemantics.raw3518step1 line 467
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical3518 line 469
  105. def OAI.MUB6.Certificate.PairSemantics.raw3519 line 482
  106. def OAI.MUB6.Certificate.PairSemantics.raw3519step0 line 484
  107. def OAI.MUB6.Certificate.PairSemantics.raw3519step1 line 486
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical3519 line 488