OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical76.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2432 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw2432step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw2432step1 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2432 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw2433 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw2433step0 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw2433step1 line 38
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical2433 line 40
  9. def OAI.MUB6.Certificate.PairSemantics.raw2434 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw2434step0 line 55
  11. def OAI.MUB6.Certificate.PairSemantics.raw2434step1 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw2434step2 line 59
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical2434 line 61
  14. def OAI.MUB6.Certificate.PairSemantics.raw2435 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw2435step0 line 80
  16. def OAI.MUB6.Certificate.PairSemantics.raw2435step1 line 82
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical2435 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw2436 line 97
  19. def OAI.MUB6.Certificate.PairSemantics.raw2436step0 line 99
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical2436 line 101
  21. def OAI.MUB6.Certificate.PairSemantics.raw2437 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw2437step0 line 112
  23. def OAI.MUB6.Certificate.PairSemantics.raw2437step1 line 114
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2437 line 116
  25. def OAI.MUB6.Certificate.PairSemantics.raw2438 line 129
  26. def OAI.MUB6.Certificate.PairSemantics.raw2438step0 line 131
  27. def OAI.MUB6.Certificate.PairSemantics.raw2438step1 line 133
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2438 line 135
  29. def OAI.MUB6.Certificate.PairSemantics.raw2439 line 148
  30. def OAI.MUB6.Certificate.PairSemantics.raw2439step0 line 150
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2439 line 152
  32. def OAI.MUB6.Certificate.PairSemantics.raw2440 line 161
  33. def OAI.MUB6.Certificate.PairSemantics.raw2440step0 line 163
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical2440 line 165
  35. def OAI.MUB6.Certificate.PairSemantics.raw2441 line 174
  36. def OAI.MUB6.Certificate.PairSemantics.raw2441step0 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw2441step1 line 178
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical2441 line 180
  39. def OAI.MUB6.Certificate.PairSemantics.raw2442 line 193
  40. def OAI.MUB6.Certificate.PairSemantics.raw2442step0 line 195
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical2442 line 197
  42. def OAI.MUB6.Certificate.PairSemantics.raw2443 line 206
  43. def OAI.MUB6.Certificate.PairSemantics.raw2443step0 line 208
  44. def OAI.MUB6.Certificate.PairSemantics.raw2443step1 line 210
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2443 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw2444 line 225
  47. def OAI.MUB6.Certificate.PairSemantics.raw2444step0 line 227
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2444 line 229
  49. def OAI.MUB6.Certificate.PairSemantics.raw2445 line 238
  50. def OAI.MUB6.Certificate.PairSemantics.raw2445step0 line 240
  51. def OAI.MUB6.Certificate.PairSemantics.raw2445step1 line 242
  52. def OAI.MUB6.Certificate.PairSemantics.raw2445step2 line 244
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical2445 line 246
  54. def OAI.MUB6.Certificate.PairSemantics.raw2446 line 263
  55. def OAI.MUB6.Certificate.PairSemantics.raw2446step0 line 265
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical2446 line 267
  57. def OAI.MUB6.Certificate.PairSemantics.raw2447 line 276
  58. def OAI.MUB6.Certificate.PairSemantics.raw2447step0 line 278
  59. def OAI.MUB6.Certificate.PairSemantics.raw2447step1 line 280
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical2447 line 282
  61. def OAI.MUB6.Certificate.PairSemantics.raw2448 line 295
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical2448 line 297
  63. def OAI.MUB6.Certificate.PairSemantics.raw2449 line 301
  64. def OAI.MUB6.Certificate.PairSemantics.raw2449step0 line 303
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical2449 line 305
  66. def OAI.MUB6.Certificate.PairSemantics.raw2450 line 314
  67. def OAI.MUB6.Certificate.PairSemantics.raw2450step0 line 316
  68. def OAI.MUB6.Certificate.PairSemantics.raw2450step1 line 318
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical2450 line 320
  70. def OAI.MUB6.Certificate.PairSemantics.raw2451 line 333
  71. def OAI.MUB6.Certificate.PairSemantics.raw2451step0 line 335
  72. def OAI.MUB6.Certificate.PairSemantics.raw2451step1 line 337
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical2451 line 339
  74. def OAI.MUB6.Certificate.PairSemantics.raw2452 line 352
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2452 line 354
  76. def OAI.MUB6.Certificate.PairSemantics.raw2453 line 358
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical2453 line 360
  78. def OAI.MUB6.Certificate.PairSemantics.raw2454 line 364
  79. def OAI.MUB6.Certificate.PairSemantics.raw2454step0 line 366
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical2454 line 368
  81. def OAI.MUB6.Certificate.PairSemantics.raw2455 line 377
  82. def OAI.MUB6.Certificate.PairSemantics.raw2455step0 line 379
  83. def OAI.MUB6.Certificate.PairSemantics.raw2455step1 line 381
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical2455 line 383
  85. def OAI.MUB6.Certificate.PairSemantics.raw2456 line 396
  86. def OAI.MUB6.Certificate.PairSemantics.raw2456step0 line 398
  87. def OAI.MUB6.Certificate.PairSemantics.raw2456step1 line 400
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical2456 line 402
  89. def OAI.MUB6.Certificate.PairSemantics.raw2457 line 415
  90. def OAI.MUB6.Certificate.PairSemantics.raw2457step0 line 417
  91. def OAI.MUB6.Certificate.PairSemantics.raw2457step1 line 419
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2457 line 421
  93. def OAI.MUB6.Certificate.PairSemantics.raw2458 line 434
  94. def OAI.MUB6.Certificate.PairSemantics.raw2458step0 line 436
  95. def OAI.MUB6.Certificate.PairSemantics.raw2458step1 line 438
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical2458 line 440
  97. def OAI.MUB6.Certificate.PairSemantics.raw2459 line 453
  98. def OAI.MUB6.Certificate.PairSemantics.raw2459step0 line 455
  99. def OAI.MUB6.Certificate.PairSemantics.raw2459step1 line 457
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical2459 line 459
  101. def OAI.MUB6.Certificate.PairSemantics.raw2460 line 472
  102. def OAI.MUB6.Certificate.PairSemantics.raw2460step0 line 474
  103. def OAI.MUB6.Certificate.PairSemantics.raw2460step1 line 476
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical2460 line 478
  105. def OAI.MUB6.Certificate.PairSemantics.raw2461 line 491
  106. def OAI.MUB6.Certificate.PairSemantics.raw2461step0 line 493
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical2461 line 495
  108. def OAI.MUB6.Certificate.PairSemantics.raw2462 line 504
  109. def OAI.MUB6.Certificate.PairSemantics.raw2462step0 line 506
  110. def OAI.MUB6.Certificate.PairSemantics.raw2462step1 line 508
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical2462 line 510
  112. def OAI.MUB6.Certificate.PairSemantics.raw2463 line 523
  113. def OAI.MUB6.Certificate.PairSemantics.raw2463step0 line 525
  114. def OAI.MUB6.Certificate.PairSemantics.raw2463step1 line 527
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical2463 line 529