OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical226.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7232 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw7232step0 line 19
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical7232 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw7233 line 30
  5. def OAI.MUB6.Certificate.PairSemantics.raw7233step0 line 32
  6. def OAI.MUB6.Certificate.PairSemantics.raw7233step1 line 34
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical7233 line 36
  8. def OAI.MUB6.Certificate.PairSemantics.raw7234 line 49
  9. def OAI.MUB6.Certificate.PairSemantics.raw7234step0 line 51
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical7234 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw7235 line 62
  12. def OAI.MUB6.Certificate.PairSemantics.raw7235step0 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw7235step1 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw7235step2 line 68
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical7235 line 70
  16. def OAI.MUB6.Certificate.PairSemantics.raw7236 line 87
  17. def OAI.MUB6.Certificate.PairSemantics.raw7236step0 line 89
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical7236 line 91
  19. def OAI.MUB6.Certificate.PairSemantics.raw7237 line 100
  20. def OAI.MUB6.Certificate.PairSemantics.raw7237step0 line 102
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical7237 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw7238 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw7238step0 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw7238step1 line 117
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical7238 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw7239 line 132
  27. def OAI.MUB6.Certificate.PairSemantics.raw7239step0 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw7239step1 line 136
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical7239 line 138
  30. def OAI.MUB6.Certificate.PairSemantics.raw7240 line 151
  31. def OAI.MUB6.Certificate.PairSemantics.raw7240step0 line 153
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical7240 line 155
  33. def OAI.MUB6.Certificate.PairSemantics.raw7241 line 164
  34. def OAI.MUB6.Certificate.PairSemantics.raw7241step0 line 166
  35. def OAI.MUB6.Certificate.PairSemantics.raw7241step1 line 168
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7241 line 170
  37. def OAI.MUB6.Certificate.PairSemantics.raw7242 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw7242step0 line 185
  39. def OAI.MUB6.Certificate.PairSemantics.raw7242step1 line 187
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7242 line 189
  41. def OAI.MUB6.Certificate.PairSemantics.raw7243 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw7243step0 line 204
  43. def OAI.MUB6.Certificate.PairSemantics.raw7243step1 line 206
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical7243 line 208
  45. def OAI.MUB6.Certificate.PairSemantics.raw7244 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw7244step0 line 223
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical7244 line 225
  48. def OAI.MUB6.Certificate.PairSemantics.raw7245 line 234
  49. def OAI.MUB6.Certificate.PairSemantics.raw7245step0 line 236
  50. def OAI.MUB6.Certificate.PairSemantics.raw7245step1 line 238
  51. def OAI.MUB6.Certificate.PairSemantics.raw7245step2 line 240
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical7245 line 242
  53. def OAI.MUB6.Certificate.PairSemantics.raw7246 line 259
  54. def OAI.MUB6.Certificate.PairSemantics.raw7246step0 line 261
  55. def OAI.MUB6.Certificate.PairSemantics.raw7246step1 line 263
  56. def OAI.MUB6.Certificate.PairSemantics.raw7246step2 line 265
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical7246 line 267
  58. def OAI.MUB6.Certificate.PairSemantics.raw7247 line 284
  59. def OAI.MUB6.Certificate.PairSemantics.raw7247step0 line 286
  60. def OAI.MUB6.Certificate.PairSemantics.raw7247step1 line 288
  61. def OAI.MUB6.Certificate.PairSemantics.raw7247step2 line 290
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7247 line 292
  63. def OAI.MUB6.Certificate.PairSemantics.raw7248 line 309
  64. def OAI.MUB6.Certificate.PairSemantics.raw7248step0 line 311
  65. def OAI.MUB6.Certificate.PairSemantics.raw7248step1 line 313
  66. def OAI.MUB6.Certificate.PairSemantics.raw7248step2 line 315
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical7248 line 317
  68. def OAI.MUB6.Certificate.PairSemantics.raw7249 line 334
  69. def OAI.MUB6.Certificate.PairSemantics.raw7249step0 line 336
  70. def OAI.MUB6.Certificate.PairSemantics.raw7249step1 line 338
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical7249 line 340
  72. def OAI.MUB6.Certificate.PairSemantics.raw7250 line 353
  73. def OAI.MUB6.Certificate.PairSemantics.raw7250step0 line 355
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7250 line 357
  75. def OAI.MUB6.Certificate.PairSemantics.raw7251 line 366
  76. def OAI.MUB6.Certificate.PairSemantics.raw7251step0 line 368
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical7251 line 370
  78. def OAI.MUB6.Certificate.PairSemantics.raw7252 line 379
  79. def OAI.MUB6.Certificate.PairSemantics.raw7252step0 line 381
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical7252 line 383
  81. def OAI.MUB6.Certificate.PairSemantics.raw7253 line 392
  82. def OAI.MUB6.Certificate.PairSemantics.raw7253step0 line 394
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical7253 line 396
  84. def OAI.MUB6.Certificate.PairSemantics.raw7254 line 405
  85. def OAI.MUB6.Certificate.PairSemantics.raw7254step0 line 407
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical7254 line 409
  87. def OAI.MUB6.Certificate.PairSemantics.raw7255 line 418
  88. def OAI.MUB6.Certificate.PairSemantics.raw7255step0 line 420
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7255 line 422
  90. def OAI.MUB6.Certificate.PairSemantics.raw7256 line 431
  91. def OAI.MUB6.Certificate.PairSemantics.raw7256step0 line 433
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical7256 line 435
  93. def OAI.MUB6.Certificate.PairSemantics.raw7257 line 444
  94. def OAI.MUB6.Certificate.PairSemantics.raw7257step0 line 446
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical7257 line 448
  96. def OAI.MUB6.Certificate.PairSemantics.raw7258 line 457
  97. def OAI.MUB6.Certificate.PairSemantics.raw7258step0 line 459
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical7258 line 461
  99. def OAI.MUB6.Certificate.PairSemantics.raw7259 line 470
  100. def OAI.MUB6.Certificate.PairSemantics.raw7259step0 line 472
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7259 line 474
  102. def OAI.MUB6.Certificate.PairSemantics.raw7260 line 483
  103. def OAI.MUB6.Certificate.PairSemantics.raw7260step0 line 485
  104. def OAI.MUB6.Certificate.PairSemantics.raw7260step1 line 487
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical7260 line 489
  106. def OAI.MUB6.Certificate.PairSemantics.raw7261 line 502
  107. def OAI.MUB6.Certificate.PairSemantics.raw7261step0 line 504
  108. def OAI.MUB6.Certificate.PairSemantics.raw7261step1 line 506
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical7261 line 508
  110. def OAI.MUB6.Certificate.PairSemantics.raw7262 line 521
  111. def OAI.MUB6.Certificate.PairSemantics.raw7262step0 line 523
  112. def OAI.MUB6.Certificate.PairSemantics.raw7262step1 line 525
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical7262 line 527
  114. def OAI.MUB6.Certificate.PairSemantics.raw7263 line 540
  115. def OAI.MUB6.Certificate.PairSemantics.raw7263step0 line 542
  116. def OAI.MUB6.Certificate.PairSemantics.raw7263step1 line 544
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical7263 line 546