OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical191.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6112 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw6112step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw6112step1 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw6112step2 line 22
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical6112 line 24
  6. def OAI.MUB6.Certificate.PairSemantics.raw6113 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw6113step0 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw6113step1 line 45
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical6113 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw6114 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw6114step0 line 62
  12. def OAI.MUB6.Certificate.PairSemantics.raw6114step1 line 64
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical6114 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw6115 line 79
  15. def OAI.MUB6.Certificate.PairSemantics.raw6115step0 line 81
  16. def OAI.MUB6.Certificate.PairSemantics.raw6115step1 line 83
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical6115 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw6116 line 98
  19. def OAI.MUB6.Certificate.PairSemantics.raw6116step0 line 100
  20. def OAI.MUB6.Certificate.PairSemantics.raw6116step1 line 102
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6116 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw6117 line 117
  23. def OAI.MUB6.Certificate.PairSemantics.raw6117step0 line 119
  24. def OAI.MUB6.Certificate.PairSemantics.raw6117step1 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw6117step2 line 123
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical6117 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw6118 line 142
  28. def OAI.MUB6.Certificate.PairSemantics.raw6118step0 line 144
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical6118 line 146
  30. def OAI.MUB6.Certificate.PairSemantics.raw6119 line 155
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical6119 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw6120 line 161
  33. def OAI.MUB6.Certificate.PairSemantics.raw6120step0 line 163
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6120 line 165
  35. def OAI.MUB6.Certificate.PairSemantics.raw6121 line 174
  36. def OAI.MUB6.Certificate.PairSemantics.raw6121step0 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw6121step1 line 178
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical6121 line 180
  39. def OAI.MUB6.Certificate.PairSemantics.raw6122 line 193
  40. def OAI.MUB6.Certificate.PairSemantics.raw6122step0 line 195
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical6122 line 197
  42. def OAI.MUB6.Certificate.PairSemantics.raw6123 line 206
  43. def OAI.MUB6.Certificate.PairSemantics.raw6123step0 line 208
  44. def OAI.MUB6.Certificate.PairSemantics.raw6123step1 line 210
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical6123 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw6124 line 225
  47. def OAI.MUB6.Certificate.PairSemantics.raw6124step0 line 227
  48. def OAI.MUB6.Certificate.PairSemantics.raw6124step1 line 229
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical6124 line 231
  50. def OAI.MUB6.Certificate.PairSemantics.raw6125 line 244
  51. def OAI.MUB6.Certificate.PairSemantics.raw6125step0 line 246
  52. def OAI.MUB6.Certificate.PairSemantics.raw6125step1 line 248
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical6125 line 250
  54. def OAI.MUB6.Certificate.PairSemantics.raw6126 line 263
  55. def OAI.MUB6.Certificate.PairSemantics.raw6126step0 line 265
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical6126 line 267
  57. def OAI.MUB6.Certificate.PairSemantics.raw6127 line 276
  58. def OAI.MUB6.Certificate.PairSemantics.raw6127step0 line 278
  59. def OAI.MUB6.Certificate.PairSemantics.raw6127step1 line 280
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6127 line 282
  61. def OAI.MUB6.Certificate.PairSemantics.raw6128 line 295
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6128 line 297
  63. def OAI.MUB6.Certificate.PairSemantics.raw6129 line 301
  64. def OAI.MUB6.Certificate.PairSemantics.raw6129step0 line 303
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical6129 line 305
  66. def OAI.MUB6.Certificate.PairSemantics.raw6130 line 314
  67. def OAI.MUB6.Certificate.PairSemantics.raw6130step0 line 316
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical6130 line 318
  69. def OAI.MUB6.Certificate.PairSemantics.raw6131 line 327
  70. def OAI.MUB6.Certificate.PairSemantics.raw6131step0 line 329
  71. def OAI.MUB6.Certificate.PairSemantics.raw6131step1 line 331
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6131 line 333
  73. def OAI.MUB6.Certificate.PairSemantics.raw6132 line 346
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6132 line 348
  75. def OAI.MUB6.Certificate.PairSemantics.raw6133 line 352
  76. def OAI.MUB6.Certificate.PairSemantics.raw6133step0 line 354
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical6133 line 356
  78. def OAI.MUB6.Certificate.PairSemantics.raw6134 line 365
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical6134 line 367
  80. def OAI.MUB6.Certificate.PairSemantics.raw6135 line 371
  81. def OAI.MUB6.Certificate.PairSemantics.raw6135step0 line 373
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical6135 line 375
  83. def OAI.MUB6.Certificate.PairSemantics.raw6136 line 384
  84. def OAI.MUB6.Certificate.PairSemantics.raw6136step0 line 386
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6136 line 388
  86. def OAI.MUB6.Certificate.PairSemantics.raw6137 line 397
  87. def OAI.MUB6.Certificate.PairSemantics.raw6137step0 line 399
  88. def OAI.MUB6.Certificate.PairSemantics.raw6137step1 line 401
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical6137 line 403
  90. def OAI.MUB6.Certificate.PairSemantics.raw6138 line 416
  91. def OAI.MUB6.Certificate.PairSemantics.raw6138step0 line 418
  92. def OAI.MUB6.Certificate.PairSemantics.raw6138step1 line 420
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical6138 line 422
  94. def OAI.MUB6.Certificate.PairSemantics.raw6139 line 435
  95. def OAI.MUB6.Certificate.PairSemantics.raw6139step0 line 437
  96. def OAI.MUB6.Certificate.PairSemantics.raw6139step1 line 439
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical6139 line 441
  98. def OAI.MUB6.Certificate.PairSemantics.raw6140 line 454
  99. def OAI.MUB6.Certificate.PairSemantics.raw6140step0 line 456
  100. def OAI.MUB6.Certificate.PairSemantics.raw6140step1 line 458
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical6140 line 460
  102. def OAI.MUB6.Certificate.PairSemantics.raw6141 line 473
  103. def OAI.MUB6.Certificate.PairSemantics.raw6141step0 line 475
  104. def OAI.MUB6.Certificate.PairSemantics.raw6141step1 line 477
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical6141 line 479
  106. def OAI.MUB6.Certificate.PairSemantics.raw6142 line 492
  107. def OAI.MUB6.Certificate.PairSemantics.raw6142step0 line 494
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical6142 line 496
  109. def OAI.MUB6.Certificate.PairSemantics.raw6143 line 505
  110. def OAI.MUB6.Certificate.PairSemantics.raw6143step0 line 507
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical6143 line 509