OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical75.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2400 line 18
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical2400 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw2401 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2401 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw2402 line 30
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical2402 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw2403 line 36
  8. def OAI.MUB6.Certificate.PairSemantics.raw2403step0 line 38
  9. def OAI.MUB6.Certificate.PairSemantics.raw2403step1 line 40
  10. def OAI.MUB6.Certificate.PairSemantics.raw2403step2 line 42
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical2403 line 44
  12. def OAI.MUB6.Certificate.PairSemantics.raw2404 line 61
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical2404 line 63
  14. def OAI.MUB6.Certificate.PairSemantics.raw2405 line 67
  15. def OAI.MUB6.Certificate.PairSemantics.raw2405step0 line 69
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical2405 line 71
  17. def OAI.MUB6.Certificate.PairSemantics.raw2406 line 80
  18. def OAI.MUB6.Certificate.PairSemantics.raw2406step0 line 82
  19. def OAI.MUB6.Certificate.PairSemantics.raw2406step1 line 84
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical2406 line 86
  21. def OAI.MUB6.Certificate.PairSemantics.raw2407 line 99
  22. def OAI.MUB6.Certificate.PairSemantics.raw2407step0 line 101
  23. def OAI.MUB6.Certificate.PairSemantics.raw2407step1 line 103
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2407 line 105
  25. def OAI.MUB6.Certificate.PairSemantics.raw2408 line 118
  26. def OAI.MUB6.Certificate.PairSemantics.raw2408step0 line 120
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2408 line 122
  28. def OAI.MUB6.Certificate.PairSemantics.raw2409 line 131
  29. def OAI.MUB6.Certificate.PairSemantics.raw2409step0 line 133
  30. def OAI.MUB6.Certificate.PairSemantics.raw2409step1 line 135
  31. def OAI.MUB6.Certificate.PairSemantics.raw2409step2 line 137
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2409 line 139
  33. def OAI.MUB6.Certificate.PairSemantics.raw2410 line 157
  34. def OAI.MUB6.Certificate.PairSemantics.raw2410step0 line 159
  35. def OAI.MUB6.Certificate.PairSemantics.raw2410step1 line 161
  36. def OAI.MUB6.Certificate.PairSemantics.raw2410step2 line 163
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical2410 line 165
  38. def OAI.MUB6.Certificate.PairSemantics.raw2411 line 183
  39. def OAI.MUB6.Certificate.PairSemantics.raw2411step0 line 185
  40. def OAI.MUB6.Certificate.PairSemantics.raw2411step1 line 187
  41. def OAI.MUB6.Certificate.PairSemantics.raw2411step2 line 189
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2411 line 191
  43. def OAI.MUB6.Certificate.PairSemantics.raw2412 line 209
  44. def OAI.MUB6.Certificate.PairSemantics.raw2412step0 line 211
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2412 line 213
  46. def OAI.MUB6.Certificate.PairSemantics.raw2413 line 222
  47. def OAI.MUB6.Certificate.PairSemantics.raw2413step0 line 224
  48. def OAI.MUB6.Certificate.PairSemantics.raw2413step1 line 226
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2413 line 228
  50. def OAI.MUB6.Certificate.PairSemantics.raw2414 line 241
  51. def OAI.MUB6.Certificate.PairSemantics.raw2414step0 line 243
  52. def OAI.MUB6.Certificate.PairSemantics.raw2414step1 line 245
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical2414 line 247
  54. def OAI.MUB6.Certificate.PairSemantics.raw2415 line 260
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2415 line 262
  56. def OAI.MUB6.Certificate.PairSemantics.raw2416 line 266
  57. def OAI.MUB6.Certificate.PairSemantics.raw2416step0 line 268
  58. def OAI.MUB6.Certificate.PairSemantics.raw2416step1 line 270
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2416 line 272
  60. def OAI.MUB6.Certificate.PairSemantics.raw2417 line 285
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical2417 line 287
  62. def OAI.MUB6.Certificate.PairSemantics.raw2418 line 291
  63. def OAI.MUB6.Certificate.PairSemantics.raw2418step0 line 293
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical2418 line 295
  65. def OAI.MUB6.Certificate.PairSemantics.raw2419 line 304
  66. def OAI.MUB6.Certificate.PairSemantics.raw2419step0 line 306
  67. def OAI.MUB6.Certificate.PairSemantics.raw2419step1 line 308
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical2419 line 310
  69. def OAI.MUB6.Certificate.PairSemantics.raw2420 line 323
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical2420 line 325
  71. def OAI.MUB6.Certificate.PairSemantics.raw2421 line 329
  72. def OAI.MUB6.Certificate.PairSemantics.raw2421step0 line 331
  73. def OAI.MUB6.Certificate.PairSemantics.raw2421step1 line 333
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical2421 line 335
  75. def OAI.MUB6.Certificate.PairSemantics.raw2422 line 348
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical2422 line 350
  77. def OAI.MUB6.Certificate.PairSemantics.raw2423 line 354
  78. def OAI.MUB6.Certificate.PairSemantics.raw2423step0 line 356
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2423 line 358
  80. def OAI.MUB6.Certificate.PairSemantics.raw2424 line 367
  81. def OAI.MUB6.Certificate.PairSemantics.raw2424step0 line 369
  82. def OAI.MUB6.Certificate.PairSemantics.raw2424step1 line 371
  83. def OAI.MUB6.Certificate.PairSemantics.raw2424step2 line 373
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical2424 line 375
  85. def OAI.MUB6.Certificate.PairSemantics.raw2425 line 392
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical2425 line 394
  87. def OAI.MUB6.Certificate.PairSemantics.raw2426 line 398
  88. def OAI.MUB6.Certificate.PairSemantics.raw2426step0 line 400
  89. def OAI.MUB6.Certificate.PairSemantics.raw2426step1 line 402
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical2426 line 404
  91. def OAI.MUB6.Certificate.PairSemantics.raw2427 line 417
  92. def OAI.MUB6.Certificate.PairSemantics.raw2427step0 line 419
  93. def OAI.MUB6.Certificate.PairSemantics.raw2427step1 line 421
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical2427 line 423
  95. def OAI.MUB6.Certificate.PairSemantics.raw2428 line 436
  96. def OAI.MUB6.Certificate.PairSemantics.raw2428step0 line 438
  97. def OAI.MUB6.Certificate.PairSemantics.raw2428step1 line 440
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical2428 line 442
  99. def OAI.MUB6.Certificate.PairSemantics.raw2429 line 455
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical2429 line 457
  101. def OAI.MUB6.Certificate.PairSemantics.raw2430 line 461
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical2430 line 463
  103. def OAI.MUB6.Certificate.PairSemantics.raw2431 line 467
  104. def OAI.MUB6.Certificate.PairSemantics.raw2431step0 line 469
  105. def OAI.MUB6.Certificate.PairSemantics.raw2431step1 line 471
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical2431 line 473