OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical72.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2304 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw2304step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw2304step1 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw2304step2 line 21
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical2304 line 23
  6. def OAI.MUB6.Certificate.PairSemantics.raw2305 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw2305step0 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw2305step1 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw2305step2 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw2305step3 line 49
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical2305 line 51
  12. def OAI.MUB6.Certificate.PairSemantics.raw2306 line 73
  13. def OAI.MUB6.Certificate.PairSemantics.raw2306step0 line 75
  14. def OAI.MUB6.Certificate.PairSemantics.raw2306step1 line 77
  15. def OAI.MUB6.Certificate.PairSemantics.raw2306step2 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw2306step3 line 81
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical2306 line 83
  18. def OAI.MUB6.Certificate.PairSemantics.raw2307 line 105
  19. def OAI.MUB6.Certificate.PairSemantics.raw2307step0 line 107
  20. def OAI.MUB6.Certificate.PairSemantics.raw2307step1 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw2307step2 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw2307step3 line 113
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical2307 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw2308 line 137
  25. def OAI.MUB6.Certificate.PairSemantics.raw2308step0 line 139
  26. def OAI.MUB6.Certificate.PairSemantics.raw2308step1 line 141
  27. def OAI.MUB6.Certificate.PairSemantics.raw2308step2 line 143
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2308 line 145
  29. def OAI.MUB6.Certificate.PairSemantics.raw2309 line 163
  30. def OAI.MUB6.Certificate.PairSemantics.raw2309step0 line 165
  31. def OAI.MUB6.Certificate.PairSemantics.raw2309step1 line 167
  32. def OAI.MUB6.Certificate.PairSemantics.raw2309step2 line 169
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical2309 line 171
  34. def OAI.MUB6.Certificate.PairSemantics.raw2310 line 189
  35. def OAI.MUB6.Certificate.PairSemantics.raw2310step0 line 191
  36. def OAI.MUB6.Certificate.PairSemantics.raw2310step1 line 193
  37. def OAI.MUB6.Certificate.PairSemantics.raw2310step2 line 195
  38. def OAI.MUB6.Certificate.PairSemantics.raw2310step3 line 197
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2310 line 199
  40. def OAI.MUB6.Certificate.PairSemantics.raw2311 line 221
  41. def OAI.MUB6.Certificate.PairSemantics.raw2311step0 line 223
  42. def OAI.MUB6.Certificate.PairSemantics.raw2311step1 line 225
  43. def OAI.MUB6.Certificate.PairSemantics.raw2311step2 line 227
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical2311 line 229
  45. def OAI.MUB6.Certificate.PairSemantics.raw2312 line 247
  46. def OAI.MUB6.Certificate.PairSemantics.raw2312step0 line 249
  47. def OAI.MUB6.Certificate.PairSemantics.raw2312step1 line 251
  48. def OAI.MUB6.Certificate.PairSemantics.raw2312step2 line 253
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2312 line 255
  50. def OAI.MUB6.Certificate.PairSemantics.raw2313 line 273
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical2313 line 275
  52. def OAI.MUB6.Certificate.PairSemantics.raw2314 line 279
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical2314 line 281
  54. def OAI.MUB6.Certificate.PairSemantics.raw2315 line 285
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2315 line 287
  56. def OAI.MUB6.Certificate.PairSemantics.raw2316 line 291
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2316 line 293
  58. def OAI.MUB6.Certificate.PairSemantics.raw2317 line 297
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2317 line 299
  60. def OAI.MUB6.Certificate.PairSemantics.raw2318 line 303
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical2318 line 305
  62. def OAI.MUB6.Certificate.PairSemantics.raw2319 line 309
  63. def OAI.MUB6.Certificate.PairSemantics.raw2319step0 line 311
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical2319 line 313
  65. def OAI.MUB6.Certificate.PairSemantics.raw2320 line 322
  66. def OAI.MUB6.Certificate.PairSemantics.raw2320step0 line 324
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical2320 line 326
  68. def OAI.MUB6.Certificate.PairSemantics.raw2321 line 335
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical2321 line 337
  70. def OAI.MUB6.Certificate.PairSemantics.raw2322 line 341
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical2322 line 343
  72. def OAI.MUB6.Certificate.PairSemantics.raw2323 line 347
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical2323 line 349
  74. def OAI.MUB6.Certificate.PairSemantics.raw2324 line 353
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2324 line 355
  76. def OAI.MUB6.Certificate.PairSemantics.raw2325 line 359
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical2325 line 361
  78. def OAI.MUB6.Certificate.PairSemantics.raw2326 line 365
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2326 line 367
  80. def OAI.MUB6.Certificate.PairSemantics.raw2327 line 371
  81. def OAI.MUB6.Certificate.PairSemantics.raw2327step0 line 373
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical2327 line 375
  83. def OAI.MUB6.Certificate.PairSemantics.raw2328 line 384
  84. def OAI.MUB6.Certificate.PairSemantics.raw2328step0 line 386
  85. def OAI.MUB6.Certificate.PairSemantics.raw2328step1 line 388
  86. def OAI.MUB6.Certificate.PairSemantics.raw2328step2 line 390
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical2328 line 392
  88. def OAI.MUB6.Certificate.PairSemantics.raw2329 line 410
  89. def OAI.MUB6.Certificate.PairSemantics.raw2329step0 line 412
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical2329 line 414
  91. def OAI.MUB6.Certificate.PairSemantics.raw2330 line 423
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2330 line 425
  93. def OAI.MUB6.Certificate.PairSemantics.raw2331 line 429
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical2331 line 431
  95. def OAI.MUB6.Certificate.PairSemantics.raw2332 line 435
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical2332 line 437
  97. def OAI.MUB6.Certificate.PairSemantics.raw2333 line 441
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical2333 line 443
  99. def OAI.MUB6.Certificate.PairSemantics.raw2334 line 447
  100. def OAI.MUB6.Certificate.PairSemantics.raw2334step0 line 449
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical2334 line 451
  102. def OAI.MUB6.Certificate.PairSemantics.raw2335 line 460
  103. def OAI.MUB6.Certificate.PairSemantics.raw2335step0 line 462
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical2335 line 464