OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical103.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3296 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw3296step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw3296step1 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw3296step2 line 21
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical3296 line 23
  6. def OAI.MUB6.Certificate.PairSemantics.raw3297 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw3297step0 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3297 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw3298 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw3298step0 line 55
  11. def OAI.MUB6.Certificate.PairSemantics.raw3298step1 line 57
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical3298 line 59
  13. def OAI.MUB6.Certificate.PairSemantics.raw3299 line 72
  14. def OAI.MUB6.Certificate.PairSemantics.raw3299step0 line 74
  15. def OAI.MUB6.Certificate.PairSemantics.raw3299step1 line 76
  16. def OAI.MUB6.Certificate.PairSemantics.raw3299step2 line 78
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical3299 line 80
  18. def OAI.MUB6.Certificate.PairSemantics.raw3300 line 97
  19. def OAI.MUB6.Certificate.PairSemantics.raw3300step0 line 99
  20. def OAI.MUB6.Certificate.PairSemantics.raw3300step1 line 101
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3300 line 103
  22. def OAI.MUB6.Certificate.PairSemantics.raw3301 line 116
  23. def OAI.MUB6.Certificate.PairSemantics.raw3301step0 line 118
  24. def OAI.MUB6.Certificate.PairSemantics.raw3301step1 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw3301step2 line 122
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical3301 line 124
  27. def OAI.MUB6.Certificate.PairSemantics.raw3302 line 141
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical3302 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw3303 line 147
  30. def OAI.MUB6.Certificate.PairSemantics.raw3303step0 line 149
  31. def OAI.MUB6.Certificate.PairSemantics.raw3303step1 line 151
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical3303 line 153
  33. def OAI.MUB6.Certificate.PairSemantics.raw3304 line 166
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical3304 line 168
  35. def OAI.MUB6.Certificate.PairSemantics.raw3305 line 172
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical3305 line 174
  37. def OAI.MUB6.Certificate.PairSemantics.raw3306 line 178
  38. def OAI.MUB6.Certificate.PairSemantics.raw3306step0 line 180
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3306 line 182
  40. def OAI.MUB6.Certificate.PairSemantics.raw3307 line 191
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical3307 line 193
  42. def OAI.MUB6.Certificate.PairSemantics.raw3308 line 197
  43. def OAI.MUB6.Certificate.PairSemantics.raw3308step0 line 199
  44. def OAI.MUB6.Certificate.PairSemantics.raw3308step1 line 201
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical3308 line 203
  46. def OAI.MUB6.Certificate.PairSemantics.raw3309 line 216
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical3309 line 218
  48. def OAI.MUB6.Certificate.PairSemantics.raw3310 line 222
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical3310 line 224
  50. def OAI.MUB6.Certificate.PairSemantics.raw3311 line 228
  51. def OAI.MUB6.Certificate.PairSemantics.raw3311step0 line 230
  52. def OAI.MUB6.Certificate.PairSemantics.raw3311step1 line 232
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3311 line 234
  54. def OAI.MUB6.Certificate.PairSemantics.raw3312 line 247
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3312 line 249
  56. def OAI.MUB6.Certificate.PairSemantics.raw3313 line 253
  57. def OAI.MUB6.Certificate.PairSemantics.raw3313step0 line 255
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical3313 line 257
  59. def OAI.MUB6.Certificate.PairSemantics.raw3314 line 266
  60. def OAI.MUB6.Certificate.PairSemantics.raw3314step0 line 268
  61. def OAI.MUB6.Certificate.PairSemantics.raw3314step1 line 270
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical3314 line 272
  63. def OAI.MUB6.Certificate.PairSemantics.raw3315 line 285
  64. def OAI.MUB6.Certificate.PairSemantics.raw3315step0 line 287
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3315 line 289
  66. def OAI.MUB6.Certificate.PairSemantics.raw3316 line 298
  67. def OAI.MUB6.Certificate.PairSemantics.raw3316step0 line 300
  68. def OAI.MUB6.Certificate.PairSemantics.raw3316step1 line 302
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3316 line 304
  70. def OAI.MUB6.Certificate.PairSemantics.raw3317 line 317
  71. def OAI.MUB6.Certificate.PairSemantics.raw3317step0 line 319
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical3317 line 321
  73. def OAI.MUB6.Certificate.PairSemantics.raw3318 line 330
  74. def OAI.MUB6.Certificate.PairSemantics.raw3318step0 line 332
  75. def OAI.MUB6.Certificate.PairSemantics.raw3318step1 line 334
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical3318 line 336
  77. def OAI.MUB6.Certificate.PairSemantics.raw3319 line 349
  78. def OAI.MUB6.Certificate.PairSemantics.raw3319step0 line 351
  79. def OAI.MUB6.Certificate.PairSemantics.raw3319step1 line 353
  80. def OAI.MUB6.Certificate.PairSemantics.raw3319step2 line 355
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical3319 line 357
  82. def OAI.MUB6.Certificate.PairSemantics.raw3320 line 374
  83. def OAI.MUB6.Certificate.PairSemantics.raw3320step0 line 376
  84. def OAI.MUB6.Certificate.PairSemantics.raw3320step1 line 378
  85. def OAI.MUB6.Certificate.PairSemantics.raw3320step2 line 380
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical3320 line 382
  87. def OAI.MUB6.Certificate.PairSemantics.raw3321 line 399
  88. def OAI.MUB6.Certificate.PairSemantics.raw3321step0 line 401
  89. def OAI.MUB6.Certificate.PairSemantics.raw3321step1 line 403
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical3321 line 405
  91. def OAI.MUB6.Certificate.PairSemantics.raw3322 line 418
  92. def OAI.MUB6.Certificate.PairSemantics.raw3322step0 line 420
  93. def OAI.MUB6.Certificate.PairSemantics.raw3322step1 line 422
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical3322 line 424
  95. def OAI.MUB6.Certificate.PairSemantics.raw3323 line 437
  96. def OAI.MUB6.Certificate.PairSemantics.raw3323step0 line 439
  97. def OAI.MUB6.Certificate.PairSemantics.raw3323step1 line 441
  98. def OAI.MUB6.Certificate.PairSemantics.raw3323step2 line 443
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical3323 line 445
  100. def OAI.MUB6.Certificate.PairSemantics.raw3324 line 462
  101. def OAI.MUB6.Certificate.PairSemantics.raw3324step0 line 464
  102. def OAI.MUB6.Certificate.PairSemantics.raw3324step1 line 466
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical3324 line 468
  104. def OAI.MUB6.Certificate.PairSemantics.raw3325 line 481
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical3325 line 483
  106. def OAI.MUB6.Certificate.PairSemantics.raw3326 line 487
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical3326 line 489
  108. def OAI.MUB6.Certificate.PairSemantics.raw3327 line 493
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical3327 line 495