OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical64.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2048 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw2048step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw2048step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2048 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw2049 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw2049step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw2049step1 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical2049 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw2050 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw2050step0 line 59
  11. def OAI.MUB6.Certificate.PairSemantics.raw2050step1 line 61
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2050 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw2051 line 76
  14. def OAI.MUB6.Certificate.PairSemantics.raw2051step0 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw2051step1 line 80
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical2051 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw2052 line 95
  18. def OAI.MUB6.Certificate.PairSemantics.raw2052step0 line 97
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical2052 line 99
  20. def OAI.MUB6.Certificate.PairSemantics.raw2053 line 108
  21. def OAI.MUB6.Certificate.PairSemantics.raw2053step0 line 110
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical2053 line 112
  23. def OAI.MUB6.Certificate.PairSemantics.raw2054 line 121
  24. def OAI.MUB6.Certificate.PairSemantics.raw2054step0 line 123
  25. def OAI.MUB6.Certificate.PairSemantics.raw2054step1 line 125
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical2054 line 127
  27. def OAI.MUB6.Certificate.PairSemantics.raw2055 line 140
  28. def OAI.MUB6.Certificate.PairSemantics.raw2055step0 line 142
  29. def OAI.MUB6.Certificate.PairSemantics.raw2055step1 line 144
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical2055 line 146
  31. def OAI.MUB6.Certificate.PairSemantics.raw2056 line 159
  32. def OAI.MUB6.Certificate.PairSemantics.raw2056step0 line 161
  33. def OAI.MUB6.Certificate.PairSemantics.raw2056step1 line 163
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical2056 line 165
  35. def OAI.MUB6.Certificate.PairSemantics.raw2057 line 178
  36. def OAI.MUB6.Certificate.PairSemantics.raw2057step0 line 180
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical2057 line 182
  38. def OAI.MUB6.Certificate.PairSemantics.raw2058 line 191
  39. def OAI.MUB6.Certificate.PairSemantics.raw2058step0 line 193
  40. def OAI.MUB6.Certificate.PairSemantics.raw2058step1 line 195
  41. def OAI.MUB6.Certificate.PairSemantics.raw2058step2 line 197
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2058 line 199
  43. def OAI.MUB6.Certificate.PairSemantics.raw2059 line 216
  44. def OAI.MUB6.Certificate.PairSemantics.raw2059step0 line 218
  45. def OAI.MUB6.Certificate.PairSemantics.raw2059step1 line 220
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical2059 line 222
  47. def OAI.MUB6.Certificate.PairSemantics.raw2060 line 235
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2060 line 237
  49. def OAI.MUB6.Certificate.PairSemantics.raw2061 line 241
  50. def OAI.MUB6.Certificate.PairSemantics.raw2061step0 line 243
  51. def OAI.MUB6.Certificate.PairSemantics.raw2061step1 line 245
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2061 line 247
  53. def OAI.MUB6.Certificate.PairSemantics.raw2062 line 260
  54. def OAI.MUB6.Certificate.PairSemantics.raw2062step0 line 262
  55. def OAI.MUB6.Certificate.PairSemantics.raw2062step1 line 264
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical2062 line 266
  57. def OAI.MUB6.Certificate.PairSemantics.raw2063 line 279
  58. def OAI.MUB6.Certificate.PairSemantics.raw2063step0 line 281
  59. def OAI.MUB6.Certificate.PairSemantics.raw2063step1 line 283
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical2063 line 285
  61. def OAI.MUB6.Certificate.PairSemantics.raw2064 line 298
  62. def OAI.MUB6.Certificate.PairSemantics.raw2064step0 line 300
  63. def OAI.MUB6.Certificate.PairSemantics.raw2064step1 line 302
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical2064 line 304
  65. def OAI.MUB6.Certificate.PairSemantics.raw2065 line 317
  66. def OAI.MUB6.Certificate.PairSemantics.raw2065step0 line 319
  67. def OAI.MUB6.Certificate.PairSemantics.raw2065step1 line 321
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical2065 line 323
  69. def OAI.MUB6.Certificate.PairSemantics.raw2066 line 336
  70. def OAI.MUB6.Certificate.PairSemantics.raw2066step0 line 338
  71. def OAI.MUB6.Certificate.PairSemantics.raw2066step1 line 340
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2066 line 342
  73. def OAI.MUB6.Certificate.PairSemantics.raw2067 line 355
  74. def OAI.MUB6.Certificate.PairSemantics.raw2067step0 line 357
  75. def OAI.MUB6.Certificate.PairSemantics.raw2067step1 line 359
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical2067 line 361
  77. def OAI.MUB6.Certificate.PairSemantics.raw2068 line 374
  78. def OAI.MUB6.Certificate.PairSemantics.raw2068step0 line 376
  79. def OAI.MUB6.Certificate.PairSemantics.raw2068step1 line 378
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical2068 line 380
  81. def OAI.MUB6.Certificate.PairSemantics.raw2069 line 393
  82. def OAI.MUB6.Certificate.PairSemantics.raw2069step0 line 395
  83. def OAI.MUB6.Certificate.PairSemantics.raw2069step1 line 397
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical2069 line 399
  85. def OAI.MUB6.Certificate.PairSemantics.raw2070 line 412
  86. def OAI.MUB6.Certificate.PairSemantics.raw2070step0 line 414
  87. def OAI.MUB6.Certificate.PairSemantics.raw2070step1 line 416
  88. def OAI.MUB6.Certificate.PairSemantics.raw2070step2 line 418
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical2070 line 420
  90. def OAI.MUB6.Certificate.PairSemantics.raw2071 line 437
  91. def OAI.MUB6.Certificate.PairSemantics.raw2071step0 line 439
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2071 line 441
  93. def OAI.MUB6.Certificate.PairSemantics.raw2072 line 450
  94. def OAI.MUB6.Certificate.PairSemantics.raw2072step0 line 452
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical2072 line 454
  96. def OAI.MUB6.Certificate.PairSemantics.raw2073 line 463
  97. def OAI.MUB6.Certificate.PairSemantics.raw2073step0 line 465
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical2073 line 467
  99. def OAI.MUB6.Certificate.PairSemantics.raw2074 line 476
  100. def OAI.MUB6.Certificate.PairSemantics.raw2074step0 line 478
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical2074 line 480
  102. def OAI.MUB6.Certificate.PairSemantics.raw2075 line 489
  103. def OAI.MUB6.Certificate.PairSemantics.raw2075step0 line 491
  104. def OAI.MUB6.Certificate.PairSemantics.raw2075step1 line 493
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical2075 line 495
  106. def OAI.MUB6.Certificate.PairSemantics.raw2076 line 508
  107. def OAI.MUB6.Certificate.PairSemantics.raw2076step0 line 510
  108. def OAI.MUB6.Certificate.PairSemantics.raw2076step1 line 512
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical2076 line 514
  110. def OAI.MUB6.Certificate.PairSemantics.raw2077 line 527
  111. def OAI.MUB6.Certificate.PairSemantics.raw2077step0 line 529
  112. def OAI.MUB6.Certificate.PairSemantics.raw2077step1 line 531
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical2077 line 533
  114. def OAI.MUB6.Certificate.PairSemantics.raw2078 line 546
  115. def OAI.MUB6.Certificate.PairSemantics.raw2078step0 line 548
  116. def OAI.MUB6.Certificate.PairSemantics.raw2078step1 line 550
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical2078 line 552
  118. def OAI.MUB6.Certificate.PairSemantics.raw2079 line 565
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical2079 line 567