OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical178.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5696 line 15
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical5696 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw5697 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5697 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw5698 line 27
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical5698 line 29
  7. def OAI.MUB6.Certificate.PairSemantics.raw5699 line 33
  8. def OAI.MUB6.Certificate.PairSemantics.raw5699step0 line 35
  9. def OAI.MUB6.Certificate.PairSemantics.raw5699step1 line 37
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical5699 line 39
  11. def OAI.MUB6.Certificate.PairSemantics.raw5700 line 52
  12. def OAI.MUB6.Certificate.PairSemantics.raw5700step0 line 54
  13. def OAI.MUB6.Certificate.PairSemantics.raw5700step1 line 56
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical5700 line 58
  15. def OAI.MUB6.Certificate.PairSemantics.raw5701 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw5701step0 line 73
  17. def OAI.MUB6.Certificate.PairSemantics.raw5701step1 line 75
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical5701 line 77
  19. def OAI.MUB6.Certificate.PairSemantics.raw5702 line 90
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical5702 line 92
  21. def OAI.MUB6.Certificate.PairSemantics.raw5703 line 96
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical5703 line 98
  23. def OAI.MUB6.Certificate.PairSemantics.raw5704 line 102
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical5704 line 104
  25. def OAI.MUB6.Certificate.PairSemantics.raw5705 line 108
  26. def OAI.MUB6.Certificate.PairSemantics.raw5705step0 line 110
  27. def OAI.MUB6.Certificate.PairSemantics.raw5705step1 line 112
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical5705 line 114
  29. def OAI.MUB6.Certificate.PairSemantics.raw5706 line 127
  30. def OAI.MUB6.Certificate.PairSemantics.raw5706step0 line 129
  31. def OAI.MUB6.Certificate.PairSemantics.raw5706step1 line 131
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5706 line 133
  33. def OAI.MUB6.Certificate.PairSemantics.raw5707 line 146
  34. def OAI.MUB6.Certificate.PairSemantics.raw5707step0 line 148
  35. def OAI.MUB6.Certificate.PairSemantics.raw5707step1 line 150
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5707 line 152
  37. def OAI.MUB6.Certificate.PairSemantics.raw5708 line 165
  38. def OAI.MUB6.Certificate.PairSemantics.raw5708step0 line 167
  39. def OAI.MUB6.Certificate.PairSemantics.raw5708step1 line 169
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical5708 line 171
  41. def OAI.MUB6.Certificate.PairSemantics.raw5709 line 184
  42. def OAI.MUB6.Certificate.PairSemantics.raw5709step0 line 186
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical5709 line 188
  44. def OAI.MUB6.Certificate.PairSemantics.raw5710 line 197
  45. def OAI.MUB6.Certificate.PairSemantics.raw5710step0 line 199
  46. def OAI.MUB6.Certificate.PairSemantics.raw5710step1 line 201
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical5710 line 203
  48. def OAI.MUB6.Certificate.PairSemantics.raw5711 line 216
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical5711 line 218
  50. def OAI.MUB6.Certificate.PairSemantics.raw5712 line 222
  51. def OAI.MUB6.Certificate.PairSemantics.raw5712step0 line 224
  52. def OAI.MUB6.Certificate.PairSemantics.raw5712step1 line 226
  53. def OAI.MUB6.Certificate.PairSemantics.raw5712step2 line 228
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical5712 line 230
  55. def OAI.MUB6.Certificate.PairSemantics.raw5713 line 247
  56. def OAI.MUB6.Certificate.PairSemantics.raw5713step0 line 249
  57. def OAI.MUB6.Certificate.PairSemantics.raw5713step1 line 251
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical5713 line 253
  59. def OAI.MUB6.Certificate.PairSemantics.raw5714 line 266
  60. def OAI.MUB6.Certificate.PairSemantics.raw5714step0 line 268
  61. def OAI.MUB6.Certificate.PairSemantics.raw5714step1 line 270
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical5714 line 272
  63. def OAI.MUB6.Certificate.PairSemantics.raw5715 line 285
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5715 line 287
  65. def OAI.MUB6.Certificate.PairSemantics.raw5716 line 291
  66. def OAI.MUB6.Certificate.PairSemantics.raw5716step0 line 293
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical5716 line 295
  68. def OAI.MUB6.Certificate.PairSemantics.raw5717 line 304
  69. def OAI.MUB6.Certificate.PairSemantics.raw5717step0 line 306
  70. def OAI.MUB6.Certificate.PairSemantics.raw5717step1 line 308
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical5717 line 310
  72. def OAI.MUB6.Certificate.PairSemantics.raw5718 line 323
  73. def OAI.MUB6.Certificate.PairSemantics.raw5718step0 line 325
  74. def OAI.MUB6.Certificate.PairSemantics.raw5718step1 line 327
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical5718 line 329
  76. def OAI.MUB6.Certificate.PairSemantics.raw5719 line 342
  77. def OAI.MUB6.Certificate.PairSemantics.raw5719step0 line 344
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical5719 line 346
  79. def OAI.MUB6.Certificate.PairSemantics.raw5720 line 355
  80. def OAI.MUB6.Certificate.PairSemantics.raw5720step0 line 357
  81. def OAI.MUB6.Certificate.PairSemantics.raw5720step1 line 359
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical5720 line 361
  83. def OAI.MUB6.Certificate.PairSemantics.raw5721 line 374
  84. def OAI.MUB6.Certificate.PairSemantics.raw5721step0 line 376
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical5721 line 378
  86. def OAI.MUB6.Certificate.PairSemantics.raw5722 line 387
  87. def OAI.MUB6.Certificate.PairSemantics.raw5722step0 line 389
  88. def OAI.MUB6.Certificate.PairSemantics.raw5722step1 line 391
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5722 line 393
  90. def OAI.MUB6.Certificate.PairSemantics.raw5723 line 406
  91. def OAI.MUB6.Certificate.PairSemantics.raw5723step0 line 408
  92. def OAI.MUB6.Certificate.PairSemantics.raw5723step1 line 410
  93. def OAI.MUB6.Certificate.PairSemantics.raw5723step2 line 412
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical5723 line 414
  95. def OAI.MUB6.Certificate.PairSemantics.raw5724 line 431
  96. def OAI.MUB6.Certificate.PairSemantics.raw5724step0 line 433
  97. def OAI.MUB6.Certificate.PairSemantics.raw5724step1 line 435
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical5724 line 437
  99. def OAI.MUB6.Certificate.PairSemantics.raw5725 line 450
  100. def OAI.MUB6.Certificate.PairSemantics.raw5725step0 line 452
  101. def OAI.MUB6.Certificate.PairSemantics.raw5725step1 line 454
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical5725 line 456
  103. def OAI.MUB6.Certificate.PairSemantics.raw5726 line 469
  104. def OAI.MUB6.Certificate.PairSemantics.raw5726step0 line 471
  105. def OAI.MUB6.Certificate.PairSemantics.raw5726step1 line 473
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical5726 line 475
  107. def OAI.MUB6.Certificate.PairSemantics.raw5727 line 488
  108. def OAI.MUB6.Certificate.PairSemantics.raw5727step0 line 490
  109. def OAI.MUB6.Certificate.PairSemantics.raw5727step1 line 492
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical5727 line 494