OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical222.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7104 line 18
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical7104 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw7105 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7105 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw7106 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw7106step0 line 32
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical7106 line 34
  8. def OAI.MUB6.Certificate.PairSemantics.raw7107 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical7107 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw7108 line 50
  11. def OAI.MUB6.Certificate.PairSemantics.raw7108step0 line 52
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical7108 line 54
  13. def OAI.MUB6.Certificate.PairSemantics.raw7109 line 64
  14. def OAI.MUB6.Certificate.PairSemantics.raw7109step0 line 66
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical7109 line 68
  16. def OAI.MUB6.Certificate.PairSemantics.raw7110 line 78
  17. def OAI.MUB6.Certificate.PairSemantics.raw7110step0 line 80
  18. def OAI.MUB6.Certificate.PairSemantics.raw7110step1 line 82
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical7110 line 84
  20. def OAI.MUB6.Certificate.PairSemantics.raw7111 line 97
  21. def OAI.MUB6.Certificate.PairSemantics.raw7111step0 line 99
  22. def OAI.MUB6.Certificate.PairSemantics.raw7111step1 line 101
  23. def OAI.MUB6.Certificate.PairSemantics.raw7111step2 line 103
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical7111 line 105
  25. def OAI.MUB6.Certificate.PairSemantics.raw7112 line 122
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical7112 line 124
  27. def OAI.MUB6.Certificate.PairSemantics.raw7113 line 128
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical7113 line 130
  29. def OAI.MUB6.Certificate.PairSemantics.raw7114 line 134
  30. def OAI.MUB6.Certificate.PairSemantics.raw7114step0 line 136
  31. def OAI.MUB6.Certificate.PairSemantics.raw7114step1 line 138
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical7114 line 140
  33. def OAI.MUB6.Certificate.PairSemantics.raw7115 line 153
  34. def OAI.MUB6.Certificate.PairSemantics.raw7115step0 line 155
  35. def OAI.MUB6.Certificate.PairSemantics.raw7115step1 line 157
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7115 line 159
  37. def OAI.MUB6.Certificate.PairSemantics.raw7116 line 172
  38. def OAI.MUB6.Certificate.PairSemantics.raw7116step0 line 174
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical7116 line 176
  40. def OAI.MUB6.Certificate.PairSemantics.raw7117 line 185
  41. def OAI.MUB6.Certificate.PairSemantics.raw7117step0 line 187
  42. def OAI.MUB6.Certificate.PairSemantics.raw7117step1 line 189
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical7117 line 191
  44. def OAI.MUB6.Certificate.PairSemantics.raw7118 line 204
  45. def OAI.MUB6.Certificate.PairSemantics.raw7118step0 line 206
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical7118 line 208
  47. def OAI.MUB6.Certificate.PairSemantics.raw7119 line 217
  48. def OAI.MUB6.Certificate.PairSemantics.raw7119step0 line 219
  49. def OAI.MUB6.Certificate.PairSemantics.raw7119step1 line 221
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical7119 line 223
  51. def OAI.MUB6.Certificate.PairSemantics.raw7120 line 236
  52. def OAI.MUB6.Certificate.PairSemantics.raw7120step0 line 238
  53. def OAI.MUB6.Certificate.PairSemantics.raw7120step1 line 240
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical7120 line 242
  55. def OAI.MUB6.Certificate.PairSemantics.raw7121 line 255
  56. def OAI.MUB6.Certificate.PairSemantics.raw7121step0 line 257
  57. def OAI.MUB6.Certificate.PairSemantics.raw7121step1 line 259
  58. def OAI.MUB6.Certificate.PairSemantics.raw7121step2 line 261
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7121 line 263
  60. def OAI.MUB6.Certificate.PairSemantics.raw7122 line 280
  61. def OAI.MUB6.Certificate.PairSemantics.raw7122step0 line 282
  62. def OAI.MUB6.Certificate.PairSemantics.raw7122step1 line 284
  63. def OAI.MUB6.Certificate.PairSemantics.raw7122step2 line 286
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical7122 line 288
  65. def OAI.MUB6.Certificate.PairSemantics.raw7123 line 305
  66. def OAI.MUB6.Certificate.PairSemantics.raw7123step0 line 307
  67. def OAI.MUB6.Certificate.PairSemantics.raw7123step1 line 309
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical7123 line 311
  69. def OAI.MUB6.Certificate.PairSemantics.raw7124 line 324
  70. def OAI.MUB6.Certificate.PairSemantics.raw7124step0 line 326
  71. def OAI.MUB6.Certificate.PairSemantics.raw7124step1 line 328
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical7124 line 330
  73. def OAI.MUB6.Certificate.PairSemantics.raw7125 line 343
  74. def OAI.MUB6.Certificate.PairSemantics.raw7125step0 line 345
  75. def OAI.MUB6.Certificate.PairSemantics.raw7125step1 line 347
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical7125 line 349
  77. def OAI.MUB6.Certificate.PairSemantics.raw7126 line 362
  78. def OAI.MUB6.Certificate.PairSemantics.raw7126step0 line 364
  79. def OAI.MUB6.Certificate.PairSemantics.raw7126step1 line 366
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical7126 line 368
  81. def OAI.MUB6.Certificate.PairSemantics.raw7127 line 381
  82. def OAI.MUB6.Certificate.PairSemantics.raw7127step0 line 383
  83. def OAI.MUB6.Certificate.PairSemantics.raw7127step1 line 385
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7127 line 387
  85. def OAI.MUB6.Certificate.PairSemantics.raw7128 line 400
  86. def OAI.MUB6.Certificate.PairSemantics.raw7128step0 line 402
  87. def OAI.MUB6.Certificate.PairSemantics.raw7128step1 line 404
  88. def OAI.MUB6.Certificate.PairSemantics.raw7128step2 line 406
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7128 line 408
  90. def OAI.MUB6.Certificate.PairSemantics.raw7129 line 425
  91. def OAI.MUB6.Certificate.PairSemantics.raw7129step0 line 427
  92. def OAI.MUB6.Certificate.PairSemantics.raw7129step1 line 429
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical7129 line 431
  94. def OAI.MUB6.Certificate.PairSemantics.raw7130 line 444
  95. def OAI.MUB6.Certificate.PairSemantics.raw7130step0 line 446
  96. def OAI.MUB6.Certificate.PairSemantics.raw7130step1 line 448
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical7130 line 450
  98. def OAI.MUB6.Certificate.PairSemantics.raw7131 line 463
  99. def OAI.MUB6.Certificate.PairSemantics.raw7131step0 line 465
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical7131 line 467
  101. def OAI.MUB6.Certificate.PairSemantics.raw7132 line 476
  102. def OAI.MUB6.Certificate.PairSemantics.raw7132step0 line 478
  103. def OAI.MUB6.Certificate.PairSemantics.raw7132step1 line 480
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical7132 line 482
  105. def OAI.MUB6.Certificate.PairSemantics.raw7133 line 495
  106. def OAI.MUB6.Certificate.PairSemantics.raw7133step0 line 497
  107. def OAI.MUB6.Certificate.PairSemantics.raw7133step1 line 499
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical7133 line 501
  109. def OAI.MUB6.Certificate.PairSemantics.raw7134 line 514
  110. def OAI.MUB6.Certificate.PairSemantics.raw7134step0 line 516
  111. def OAI.MUB6.Certificate.PairSemantics.raw7134step1 line 518
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical7134 line 520
  113. def OAI.MUB6.Certificate.PairSemantics.raw7135 line 533
  114. def OAI.MUB6.Certificate.PairSemantics.raw7135step0 line 535
  115. def OAI.MUB6.Certificate.PairSemantics.raw7135step1 line 537
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical7135 line 539