OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical228.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7296 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw7296step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw7296step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7296 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw7297 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw7297step0 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw7297step1 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7297 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw7298 line 54
  10. def OAI.MUB6.Certificate.PairSemantics.raw7298step0 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw7298step1 line 58
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical7298 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw7299 line 73
  14. def OAI.MUB6.Certificate.PairSemantics.raw7299step0 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw7299step1 line 77
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7299 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw7300 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw7300step0 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw7300step1 line 96
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical7300 line 98
  21. def OAI.MUB6.Certificate.PairSemantics.raw7301 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw7301step0 line 113
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical7301 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw7302 line 124
  25. def OAI.MUB6.Certificate.PairSemantics.raw7302step0 line 126
  26. def OAI.MUB6.Certificate.PairSemantics.raw7302step1 line 128
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical7302 line 130
  28. def OAI.MUB6.Certificate.PairSemantics.raw7303 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw7303step0 line 145
  30. def OAI.MUB6.Certificate.PairSemantics.raw7303step1 line 147
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical7303 line 149
  32. def OAI.MUB6.Certificate.PairSemantics.raw7304 line 162
  33. def OAI.MUB6.Certificate.PairSemantics.raw7304step0 line 164
  34. def OAI.MUB6.Certificate.PairSemantics.raw7304step1 line 166
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical7304 line 168
  36. def OAI.MUB6.Certificate.PairSemantics.raw7305 line 181
  37. def OAI.MUB6.Certificate.PairSemantics.raw7305step0 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw7305step1 line 185
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical7305 line 187
  40. def OAI.MUB6.Certificate.PairSemantics.raw7306 line 200
  41. def OAI.MUB6.Certificate.PairSemantics.raw7306step0 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw7306step1 line 204
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical7306 line 206
  44. def OAI.MUB6.Certificate.PairSemantics.raw7307 line 219
  45. def OAI.MUB6.Certificate.PairSemantics.raw7307step0 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw7307step1 line 223
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical7307 line 225
  48. def OAI.MUB6.Certificate.PairSemantics.raw7308 line 238
  49. def OAI.MUB6.Certificate.PairSemantics.raw7308step0 line 240
  50. def OAI.MUB6.Certificate.PairSemantics.raw7308step1 line 242
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical7308 line 244
  52. def OAI.MUB6.Certificate.PairSemantics.raw7309 line 257
  53. def OAI.MUB6.Certificate.PairSemantics.raw7309step0 line 259
  54. def OAI.MUB6.Certificate.PairSemantics.raw7309step1 line 261
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical7309 line 263
  56. def OAI.MUB6.Certificate.PairSemantics.raw7310 line 276
  57. def OAI.MUB6.Certificate.PairSemantics.raw7310step0 line 278
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical7310 line 280
  59. def OAI.MUB6.Certificate.PairSemantics.raw7311 line 289
  60. def OAI.MUB6.Certificate.PairSemantics.raw7311step0 line 291
  61. def OAI.MUB6.Certificate.PairSemantics.raw7311step1 line 293
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7311 line 295
  63. def OAI.MUB6.Certificate.PairSemantics.raw7312 line 308
  64. def OAI.MUB6.Certificate.PairSemantics.raw7312step0 line 310
  65. def OAI.MUB6.Certificate.PairSemantics.raw7312step1 line 312
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7312 line 314
  67. def OAI.MUB6.Certificate.PairSemantics.raw7313 line 327
  68. def OAI.MUB6.Certificate.PairSemantics.raw7313step0 line 329
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical7313 line 331
  70. def OAI.MUB6.Certificate.PairSemantics.raw7314 line 340
  71. def OAI.MUB6.Certificate.PairSemantics.raw7314step0 line 342
  72. def OAI.MUB6.Certificate.PairSemantics.raw7314step1 line 344
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical7314 line 346
  74. def OAI.MUB6.Certificate.PairSemantics.raw7315 line 359
  75. def OAI.MUB6.Certificate.PairSemantics.raw7315step0 line 361
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical7315 line 363
  77. def OAI.MUB6.Certificate.PairSemantics.raw7316 line 372
  78. def OAI.MUB6.Certificate.PairSemantics.raw7316step0 line 374
  79. def OAI.MUB6.Certificate.PairSemantics.raw7316step1 line 376
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical7316 line 378
  81. def OAI.MUB6.Certificate.PairSemantics.raw7317 line 391
  82. def OAI.MUB6.Certificate.PairSemantics.raw7317step0 line 393
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical7317 line 395
  84. def OAI.MUB6.Certificate.PairSemantics.raw7318 line 404
  85. def OAI.MUB6.Certificate.PairSemantics.raw7318step0 line 406
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical7318 line 408
  87. def OAI.MUB6.Certificate.PairSemantics.raw7319 line 417
  88. def OAI.MUB6.Certificate.PairSemantics.raw7319step0 line 419
  89. def OAI.MUB6.Certificate.PairSemantics.raw7319step1 line 421
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical7319 line 423
  91. def OAI.MUB6.Certificate.PairSemantics.raw7320 line 436
  92. def OAI.MUB6.Certificate.PairSemantics.raw7320step0 line 438
  93. def OAI.MUB6.Certificate.PairSemantics.raw7320step1 line 440
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical7320 line 442
  95. def OAI.MUB6.Certificate.PairSemantics.raw7321 line 455
  96. def OAI.MUB6.Certificate.PairSemantics.raw7321step0 line 457
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical7321 line 459
  98. def OAI.MUB6.Certificate.PairSemantics.raw7322 line 468
  99. def OAI.MUB6.Certificate.PairSemantics.raw7322step0 line 470
  100. def OAI.MUB6.Certificate.PairSemantics.raw7322step1 line 472
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7322 line 474
  102. def OAI.MUB6.Certificate.PairSemantics.raw7323 line 487
  103. def OAI.MUB6.Certificate.PairSemantics.raw7323step0 line 489
  104. def OAI.MUB6.Certificate.PairSemantics.raw7323step1 line 491
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical7323 line 493
  106. def OAI.MUB6.Certificate.PairSemantics.raw7324 line 506
  107. def OAI.MUB6.Certificate.PairSemantics.raw7324step0 line 508
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical7324 line 510
  109. def OAI.MUB6.Certificate.PairSemantics.raw7325 line 519
  110. def OAI.MUB6.Certificate.PairSemantics.raw7325step0 line 521
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical7325 line 523
  112. def OAI.MUB6.Certificate.PairSemantics.raw7326 line 532
  113. def OAI.MUB6.Certificate.PairSemantics.raw7326step0 line 534
  114. def OAI.MUB6.Certificate.PairSemantics.raw7326step1 line 536
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical7326 line 538
  116. def OAI.MUB6.Certificate.PairSemantics.raw7327 line 551
  117. def OAI.MUB6.Certificate.PairSemantics.raw7327step0 line 553
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical7327 line 555