OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical288.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9216 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw9216step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw9216step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical9216 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw9217 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw9217step0 line 41
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical9217 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw9218 line 52
  9. def OAI.MUB6.Certificate.PairSemantics.raw9218step0 line 54
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical9218 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw9219 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw9219step0 line 67
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical9219 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw9220 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw9220step0 line 80
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical9220 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw9221 line 91
  18. def OAI.MUB6.Certificate.PairSemantics.raw9221step0 line 93
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9221 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw9222 line 104
  21. def OAI.MUB6.Certificate.PairSemantics.raw9222step0 line 106
  22. def OAI.MUB6.Certificate.PairSemantics.raw9222step1 line 108
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical9222 line 110
  24. def OAI.MUB6.Certificate.PairSemantics.raw9223 line 123
  25. def OAI.MUB6.Certificate.PairSemantics.raw9223step0 line 125
  26. def OAI.MUB6.Certificate.PairSemantics.raw9223step1 line 127
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical9223 line 129
  28. def OAI.MUB6.Certificate.PairSemantics.raw9224 line 142
  29. def OAI.MUB6.Certificate.PairSemantics.raw9224step0 line 144
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical9224 line 146
  31. def OAI.MUB6.Certificate.PairSemantics.raw9225 line 155
  32. def OAI.MUB6.Certificate.PairSemantics.raw9225step0 line 157
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical9225 line 159
  34. def OAI.MUB6.Certificate.PairSemantics.raw9226 line 168
  35. def OAI.MUB6.Certificate.PairSemantics.raw9226step0 line 170
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical9226 line 172
  37. def OAI.MUB6.Certificate.PairSemantics.raw9227 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw9227step0 line 183
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical9227 line 185
  40. def OAI.MUB6.Certificate.PairSemantics.raw9228 line 194
  41. def OAI.MUB6.Certificate.PairSemantics.raw9228step0 line 196
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical9228 line 198
  43. def OAI.MUB6.Certificate.PairSemantics.raw9229 line 207
  44. def OAI.MUB6.Certificate.PairSemantics.raw9229step0 line 209
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical9229 line 211
  46. def OAI.MUB6.Certificate.PairSemantics.raw9230 line 220
  47. def OAI.MUB6.Certificate.PairSemantics.raw9230step0 line 222
  48. def OAI.MUB6.Certificate.PairSemantics.raw9230step1 line 224
  49. def OAI.MUB6.Certificate.PairSemantics.raw9230step2 line 226
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9230 line 228
  51. def OAI.MUB6.Certificate.PairSemantics.raw9231 line 247
  52. def OAI.MUB6.Certificate.PairSemantics.raw9231step0 line 249
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9231 line 251
  54. def OAI.MUB6.Certificate.PairSemantics.raw9232 line 260
  55. def OAI.MUB6.Certificate.PairSemantics.raw9232step0 line 262
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical9232 line 264
  57. def OAI.MUB6.Certificate.PairSemantics.raw9233 line 273
  58. def OAI.MUB6.Certificate.PairSemantics.raw9233step0 line 275
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9233 line 277
  60. def OAI.MUB6.Certificate.PairSemantics.raw9234 line 286
  61. def OAI.MUB6.Certificate.PairSemantics.raw9234step0 line 288
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical9234 line 290
  63. def OAI.MUB6.Certificate.PairSemantics.raw9235 line 299
  64. def OAI.MUB6.Certificate.PairSemantics.raw9235step0 line 301
  65. def OAI.MUB6.Certificate.PairSemantics.raw9235step1 line 303
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical9235 line 305
  67. def OAI.MUB6.Certificate.PairSemantics.raw9236 line 318
  68. def OAI.MUB6.Certificate.PairSemantics.raw9236step0 line 320
  69. def OAI.MUB6.Certificate.PairSemantics.raw9236step1 line 322
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical9236 line 324
  71. def OAI.MUB6.Certificate.PairSemantics.raw9237 line 337
  72. def OAI.MUB6.Certificate.PairSemantics.raw9237step0 line 339
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical9237 line 341
  74. def OAI.MUB6.Certificate.PairSemantics.raw9238 line 350
  75. def OAI.MUB6.Certificate.PairSemantics.raw9238step0 line 352
  76. def OAI.MUB6.Certificate.PairSemantics.raw9238step1 line 354
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical9238 line 356
  78. def OAI.MUB6.Certificate.PairSemantics.raw9239 line 369
  79. def OAI.MUB6.Certificate.PairSemantics.raw9239step0 line 371
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical9239 line 373
  81. def OAI.MUB6.Certificate.PairSemantics.raw9240 line 382
  82. def OAI.MUB6.Certificate.PairSemantics.raw9240step0 line 384
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical9240 line 386
  84. def OAI.MUB6.Certificate.PairSemantics.raw9241 line 395
  85. def OAI.MUB6.Certificate.PairSemantics.raw9241step0 line 397
  86. def OAI.MUB6.Certificate.PairSemantics.raw9241step1 line 399
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical9241 line 401
  88. def OAI.MUB6.Certificate.PairSemantics.raw9242 line 414
  89. def OAI.MUB6.Certificate.PairSemantics.raw9242step0 line 416
  90. def OAI.MUB6.Certificate.PairSemantics.raw9242step1 line 418
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical9242 line 420
  92. def OAI.MUB6.Certificate.PairSemantics.raw9243 line 433
  93. def OAI.MUB6.Certificate.PairSemantics.raw9243step0 line 435
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical9243 line 437
  95. def OAI.MUB6.Certificate.PairSemantics.raw9244 line 446
  96. def OAI.MUB6.Certificate.PairSemantics.raw9244step0 line 448
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical9244 line 450
  98. def OAI.MUB6.Certificate.PairSemantics.raw9245 line 459
  99. def OAI.MUB6.Certificate.PairSemantics.raw9245step0 line 461
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical9245 line 463
  101. def OAI.MUB6.Certificate.PairSemantics.raw9246 line 472
  102. def OAI.MUB6.Certificate.PairSemantics.raw9246step0 line 474
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical9246 line 476
  104. def OAI.MUB6.Certificate.PairSemantics.raw9247 line 485
  105. def OAI.MUB6.Certificate.PairSemantics.raw9247step0 line 487
  106. def OAI.MUB6.Certificate.PairSemantics.raw9247step1 line 489
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical9247 line 491