OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical256.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8192 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw8192step0 line 21
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8192 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw8193 line 32
  5. def OAI.MUB6.Certificate.PairSemantics.raw8193step0 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw8193step1 line 36
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical8193 line 38
  8. def OAI.MUB6.Certificate.PairSemantics.raw8194 line 51
  9. def OAI.MUB6.Certificate.PairSemantics.raw8194step0 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw8194step1 line 55
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical8194 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw8195 line 70
  13. def OAI.MUB6.Certificate.PairSemantics.raw8195step0 line 72
  14. def OAI.MUB6.Certificate.PairSemantics.raw8195step1 line 74
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical8195 line 76
  16. def OAI.MUB6.Certificate.PairSemantics.raw8196 line 91
  17. def OAI.MUB6.Certificate.PairSemantics.raw8196step0 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw8196step1 line 95
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical8196 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw8197 line 111
  21. def OAI.MUB6.Certificate.PairSemantics.raw8197step0 line 113
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical8197 line 115
  23. def OAI.MUB6.Certificate.PairSemantics.raw8198 line 124
  24. def OAI.MUB6.Certificate.PairSemantics.raw8198step0 line 126
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8198 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw8199 line 137
  27. def OAI.MUB6.Certificate.PairSemantics.raw8199step0 line 139
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical8199 line 141
  29. def OAI.MUB6.Certificate.PairSemantics.raw8200 line 150
  30. def OAI.MUB6.Certificate.PairSemantics.raw8200step0 line 152
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical8200 line 154
  32. def OAI.MUB6.Certificate.PairSemantics.raw8201 line 163
  33. def OAI.MUB6.Certificate.PairSemantics.raw8201step0 line 165
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical8201 line 167
  35. def OAI.MUB6.Certificate.PairSemantics.raw8202 line 176
  36. def OAI.MUB6.Certificate.PairSemantics.raw8202step0 line 178
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical8202 line 180
  38. def OAI.MUB6.Certificate.PairSemantics.raw8203 line 189
  39. def OAI.MUB6.Certificate.PairSemantics.raw8203step0 line 191
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical8203 line 193
  41. def OAI.MUB6.Certificate.PairSemantics.raw8204 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw8204step0 line 204
  43. def OAI.MUB6.Certificate.PairSemantics.raw8204step1 line 206
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical8204 line 208
  45. def OAI.MUB6.Certificate.PairSemantics.raw8205 line 222
  46. def OAI.MUB6.Certificate.PairSemantics.raw8205step0 line 224
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical8205 line 226
  48. def OAI.MUB6.Certificate.PairSemantics.raw8206 line 235
  49. def OAI.MUB6.Certificate.PairSemantics.raw8206step0 line 237
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical8206 line 239
  51. def OAI.MUB6.Certificate.PairSemantics.raw8207 line 248
  52. def OAI.MUB6.Certificate.PairSemantics.raw8207step0 line 250
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8207 line 252
  54. def OAI.MUB6.Certificate.PairSemantics.raw8208 line 261
  55. def OAI.MUB6.Certificate.PairSemantics.raw8208step0 line 263
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical8208 line 265
  57. def OAI.MUB6.Certificate.PairSemantics.raw8209 line 274
  58. def OAI.MUB6.Certificate.PairSemantics.raw8209step0 line 276
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical8209 line 278
  60. def OAI.MUB6.Certificate.PairSemantics.raw8210 line 287
  61. def OAI.MUB6.Certificate.PairSemantics.raw8210step0 line 289
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8210 line 291
  63. def OAI.MUB6.Certificate.PairSemantics.raw8211 line 300
  64. def OAI.MUB6.Certificate.PairSemantics.raw8211step0 line 302
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical8211 line 304
  66. def OAI.MUB6.Certificate.PairSemantics.raw8212 line 313
  67. def OAI.MUB6.Certificate.PairSemantics.raw8212step0 line 315
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical8212 line 317
  69. def OAI.MUB6.Certificate.PairSemantics.raw8213 line 326
  70. def OAI.MUB6.Certificate.PairSemantics.raw8213step0 line 328
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical8213 line 330
  72. def OAI.MUB6.Certificate.PairSemantics.raw8214 line 339
  73. def OAI.MUB6.Certificate.PairSemantics.raw8214step0 line 341
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical8214 line 343
  75. def OAI.MUB6.Certificate.PairSemantics.raw8215 line 352
  76. def OAI.MUB6.Certificate.PairSemantics.raw8215step0 line 354
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical8215 line 356
  78. def OAI.MUB6.Certificate.PairSemantics.raw8216 line 366
  79. def OAI.MUB6.Certificate.PairSemantics.raw8216step0 line 368
  80. def OAI.MUB6.Certificate.PairSemantics.raw8216step1 line 370
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical8216 line 372
  82. def OAI.MUB6.Certificate.PairSemantics.raw8217 line 387
  83. def OAI.MUB6.Certificate.PairSemantics.raw8217step0 line 389
  84. def OAI.MUB6.Certificate.PairSemantics.raw8217step1 line 391
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical8217 line 393
  86. def OAI.MUB6.Certificate.PairSemantics.raw8218 line 407
  87. def OAI.MUB6.Certificate.PairSemantics.raw8218step0 line 409
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical8218 line 411
  89. def OAI.MUB6.Certificate.PairSemantics.raw8219 line 420
  90. def OAI.MUB6.Certificate.PairSemantics.raw8219step0 line 422
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical8219 line 424
  92. def OAI.MUB6.Certificate.PairSemantics.raw8220 line 433
  93. def OAI.MUB6.Certificate.PairSemantics.raw8220step0 line 435
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8220 line 437
  95. def OAI.MUB6.Certificate.PairSemantics.raw8221 line 446
  96. def OAI.MUB6.Certificate.PairSemantics.raw8221step0 line 448
  97. def OAI.MUB6.Certificate.PairSemantics.raw8221step1 line 450
  98. def OAI.MUB6.Certificate.PairSemantics.raw8221step2 line 452
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical8221 line 454
  100. def OAI.MUB6.Certificate.PairSemantics.raw8222 line 471
  101. def OAI.MUB6.Certificate.PairSemantics.raw8222step0 line 473
  102. def OAI.MUB6.Certificate.PairSemantics.raw8222step1 line 475
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical8222 line 477
  104. def OAI.MUB6.Certificate.PairSemantics.raw8223 line 490
  105. def OAI.MUB6.Certificate.PairSemantics.raw8223step0 line 492
  106. def OAI.MUB6.Certificate.PairSemantics.raw8223step1 line 494
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical8223 line 496