OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical166.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5312 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw5312step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw5312step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5312 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw5313 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw5313step0 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw5313step1 line 43
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5313 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw5314 line 58
  10. def OAI.MUB6.Certificate.PairSemantics.raw5314step0 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw5314step1 line 62
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical5314 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw5315 line 77
  14. def OAI.MUB6.Certificate.PairSemantics.raw5315step0 line 79
  15. def OAI.MUB6.Certificate.PairSemantics.raw5315step1 line 81
  16. def OAI.MUB6.Certificate.PairSemantics.raw5315step2 line 83
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical5315 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw5316 line 102
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5316 line 104
  20. def OAI.MUB6.Certificate.PairSemantics.raw5317 line 108
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical5317 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw5318 line 114
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical5318 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw5319 line 120
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical5319 line 122
  26. def OAI.MUB6.Certificate.PairSemantics.raw5320 line 126
  27. def OAI.MUB6.Certificate.PairSemantics.raw5320step0 line 128
  28. def OAI.MUB6.Certificate.PairSemantics.raw5320step1 line 130
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical5320 line 132
  30. def OAI.MUB6.Certificate.PairSemantics.raw5321 line 145
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical5321 line 147
  32. def OAI.MUB6.Certificate.PairSemantics.raw5322 line 151
  33. def OAI.MUB6.Certificate.PairSemantics.raw5322step0 line 153
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical5322 line 155
  35. def OAI.MUB6.Certificate.PairSemantics.raw5323 line 164
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5323 line 166
  37. def OAI.MUB6.Certificate.PairSemantics.raw5324 line 170
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical5324 line 172
  39. def OAI.MUB6.Certificate.PairSemantics.raw5325 line 176
  40. def OAI.MUB6.Certificate.PairSemantics.raw5325step0 line 178
  41. def OAI.MUB6.Certificate.PairSemantics.raw5325step1 line 180
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical5325 line 182
  43. def OAI.MUB6.Certificate.PairSemantics.raw5326 line 195
  44. def OAI.MUB6.Certificate.PairSemantics.raw5326step0 line 197
  45. def OAI.MUB6.Certificate.PairSemantics.raw5326step1 line 199
  46. def OAI.MUB6.Certificate.PairSemantics.raw5326step2 line 201
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical5326 line 203
  48. def OAI.MUB6.Certificate.PairSemantics.raw5327 line 220
  49. def OAI.MUB6.Certificate.PairSemantics.raw5327step0 line 222
  50. def OAI.MUB6.Certificate.PairSemantics.raw5327step1 line 224
  51. def OAI.MUB6.Certificate.PairSemantics.raw5327step2 line 226
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical5327 line 228
  53. def OAI.MUB6.Certificate.PairSemantics.raw5328 line 245
  54. def OAI.MUB6.Certificate.PairSemantics.raw5328step0 line 247
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5328 line 249
  56. def OAI.MUB6.Certificate.PairSemantics.raw5329 line 258
  57. def OAI.MUB6.Certificate.PairSemantics.raw5329step0 line 260
  58. def OAI.MUB6.Certificate.PairSemantics.raw5329step1 line 262
  59. def OAI.MUB6.Certificate.PairSemantics.raw5329step2 line 264
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical5329 line 266
  61. def OAI.MUB6.Certificate.PairSemantics.raw5330 line 283
  62. def OAI.MUB6.Certificate.PairSemantics.raw5330step0 line 285
  63. def OAI.MUB6.Certificate.PairSemantics.raw5330step1 line 287
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5330 line 289
  65. def OAI.MUB6.Certificate.PairSemantics.raw5331 line 302
  66. def OAI.MUB6.Certificate.PairSemantics.raw5331step0 line 304
  67. def OAI.MUB6.Certificate.PairSemantics.raw5331step1 line 306
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical5331 line 308
  69. def OAI.MUB6.Certificate.PairSemantics.raw5332 line 321
  70. def OAI.MUB6.Certificate.PairSemantics.raw5332step0 line 323
  71. def OAI.MUB6.Certificate.PairSemantics.raw5332step1 line 325
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical5332 line 327
  73. def OAI.MUB6.Certificate.PairSemantics.raw5333 line 340
  74. def OAI.MUB6.Certificate.PairSemantics.raw5333step0 line 342
  75. def OAI.MUB6.Certificate.PairSemantics.raw5333step1 line 344
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical5333 line 346
  77. def OAI.MUB6.Certificate.PairSemantics.raw5334 line 359
  78. def OAI.MUB6.Certificate.PairSemantics.raw5334step0 line 361
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5334 line 363
  80. def OAI.MUB6.Certificate.PairSemantics.raw5335 line 372
  81. def OAI.MUB6.Certificate.PairSemantics.raw5335step0 line 374
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical5335 line 376
  83. def OAI.MUB6.Certificate.PairSemantics.raw5336 line 385
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5336 line 387
  85. def OAI.MUB6.Certificate.PairSemantics.raw5337 line 391
  86. def OAI.MUB6.Certificate.PairSemantics.raw5337step0 line 393
  87. def OAI.MUB6.Certificate.PairSemantics.raw5337step1 line 395
  88. def OAI.MUB6.Certificate.PairSemantics.raw5337step2 line 397
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5337 line 399
  90. def OAI.MUB6.Certificate.PairSemantics.raw5338 line 417
  91. def OAI.MUB6.Certificate.PairSemantics.raw5338step0 line 419
  92. def OAI.MUB6.Certificate.PairSemantics.raw5338step1 line 421
  93. def OAI.MUB6.Certificate.PairSemantics.raw5338step2 line 423
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical5338 line 425
  95. def OAI.MUB6.Certificate.PairSemantics.raw5339 line 443
  96. def OAI.MUB6.Certificate.PairSemantics.raw5339step0 line 445
  97. def OAI.MUB6.Certificate.PairSemantics.raw5339step1 line 447
  98. def OAI.MUB6.Certificate.PairSemantics.raw5339step2 line 449
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical5339 line 451
  100. def OAI.MUB6.Certificate.PairSemantics.raw5340 line 469
  101. def OAI.MUB6.Certificate.PairSemantics.raw5340step0 line 471
  102. def OAI.MUB6.Certificate.PairSemantics.raw5340step1 line 473
  103. def OAI.MUB6.Certificate.PairSemantics.raw5340step2 line 475
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical5340 line 477
  105. def OAI.MUB6.Certificate.PairSemantics.raw5341 line 495
  106. def OAI.MUB6.Certificate.PairSemantics.raw5341step0 line 497
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical5341 line 499
  108. def OAI.MUB6.Certificate.PairSemantics.raw5342 line 508
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical5342 line 510
  110. def OAI.MUB6.Certificate.PairSemantics.raw5343 line 514
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical5343 line 516