OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical206.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6592 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw6592step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw6592step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical6592 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw6593 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw6593step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw6593step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6593 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw6594 line 59
  10. def OAI.MUB6.Certificate.PairSemantics.raw6594step0 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw6594step1 line 63
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical6594 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw6595 line 78
  14. def OAI.MUB6.Certificate.PairSemantics.raw6595step0 line 80
  15. def OAI.MUB6.Certificate.PairSemantics.raw6595step1 line 82
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical6595 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw6596 line 97
  18. def OAI.MUB6.Certificate.PairSemantics.raw6596step0 line 99
  19. def OAI.MUB6.Certificate.PairSemantics.raw6596step1 line 101
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical6596 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw6597 line 116
  22. def OAI.MUB6.Certificate.PairSemantics.raw6597step0 line 118
  23. def OAI.MUB6.Certificate.PairSemantics.raw6597step1 line 120
  24. def OAI.MUB6.Certificate.PairSemantics.raw6597step2 line 122
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical6597 line 124
  26. def OAI.MUB6.Certificate.PairSemantics.raw6598 line 141
  27. def OAI.MUB6.Certificate.PairSemantics.raw6598step0 line 143
  28. def OAI.MUB6.Certificate.PairSemantics.raw6598step1 line 145
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical6598 line 147
  30. def OAI.MUB6.Certificate.PairSemantics.raw6599 line 160
  31. def OAI.MUB6.Certificate.PairSemantics.raw6599step0 line 162
  32. def OAI.MUB6.Certificate.PairSemantics.raw6599step1 line 164
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical6599 line 166
  34. def OAI.MUB6.Certificate.PairSemantics.raw6600 line 179
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical6600 line 181
  36. def OAI.MUB6.Certificate.PairSemantics.raw6601 line 185
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical6601 line 187
  38. def OAI.MUB6.Certificate.PairSemantics.raw6602 line 191
  39. def OAI.MUB6.Certificate.PairSemantics.raw6602step0 line 193
  40. def OAI.MUB6.Certificate.PairSemantics.raw6602step1 line 195
  41. def OAI.MUB6.Certificate.PairSemantics.raw6602step2 line 197
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical6602 line 199
  43. def OAI.MUB6.Certificate.PairSemantics.raw6603 line 216
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical6603 line 218
  45. def OAI.MUB6.Certificate.PairSemantics.raw6604 line 222
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical6604 line 224
  47. def OAI.MUB6.Certificate.PairSemantics.raw6605 line 228
  48. def OAI.MUB6.Certificate.PairSemantics.raw6605step0 line 230
  49. def OAI.MUB6.Certificate.PairSemantics.raw6605step1 line 232
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical6605 line 234
  51. def OAI.MUB6.Certificate.PairSemantics.raw6606 line 247
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6606 line 249
  53. def OAI.MUB6.Certificate.PairSemantics.raw6607 line 253
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical6607 line 255
  55. def OAI.MUB6.Certificate.PairSemantics.raw6608 line 259
  56. def OAI.MUB6.Certificate.PairSemantics.raw6608step0 line 261
  57. def OAI.MUB6.Certificate.PairSemantics.raw6608step1 line 263
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical6608 line 265
  59. def OAI.MUB6.Certificate.PairSemantics.raw6609 line 278
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6609 line 280
  61. def OAI.MUB6.Certificate.PairSemantics.raw6610 line 284
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6610 line 286
  63. def OAI.MUB6.Certificate.PairSemantics.raw6611 line 290
  64. def OAI.MUB6.Certificate.PairSemantics.raw6611step0 line 292
  65. def OAI.MUB6.Certificate.PairSemantics.raw6611step1 line 294
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical6611 line 296
  67. def OAI.MUB6.Certificate.PairSemantics.raw6612 line 309
  68. def OAI.MUB6.Certificate.PairSemantics.raw6612step0 line 311
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6612 line 313
  70. def OAI.MUB6.Certificate.PairSemantics.raw6613 line 322
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical6613 line 324
  72. def OAI.MUB6.Certificate.PairSemantics.raw6614 line 328
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical6614 line 330
  74. def OAI.MUB6.Certificate.PairSemantics.raw6615 line 334
  75. def OAI.MUB6.Certificate.PairSemantics.raw6615step0 line 336
  76. def OAI.MUB6.Certificate.PairSemantics.raw6615step1 line 338
  77. def OAI.MUB6.Certificate.PairSemantics.raw6615step2 line 340
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6615 line 342
  79. def OAI.MUB6.Certificate.PairSemantics.raw6616 line 359
  80. def OAI.MUB6.Certificate.PairSemantics.raw6616step0 line 361
  81. def OAI.MUB6.Certificate.PairSemantics.raw6616step1 line 363
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical6616 line 365
  83. def OAI.MUB6.Certificate.PairSemantics.raw6617 line 378
  84. def OAI.MUB6.Certificate.PairSemantics.raw6617step0 line 380
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6617 line 382
  86. def OAI.MUB6.Certificate.PairSemantics.raw6618 line 391
  87. def OAI.MUB6.Certificate.PairSemantics.raw6618step0 line 393
  88. def OAI.MUB6.Certificate.PairSemantics.raw6618step1 line 395
  89. def OAI.MUB6.Certificate.PairSemantics.raw6618step2 line 397
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical6618 line 399
  91. def OAI.MUB6.Certificate.PairSemantics.raw6619 line 416
  92. def OAI.MUB6.Certificate.PairSemantics.raw6619step0 line 418
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical6619 line 420
  94. def OAI.MUB6.Certificate.PairSemantics.raw6620 line 429
  95. def OAI.MUB6.Certificate.PairSemantics.raw6620step0 line 431
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical6620 line 433
  97. def OAI.MUB6.Certificate.PairSemantics.raw6621 line 442
  98. def OAI.MUB6.Certificate.PairSemantics.raw6621step0 line 444
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical6621 line 446
  100. def OAI.MUB6.Certificate.PairSemantics.raw6622 line 455
  101. def OAI.MUB6.Certificate.PairSemantics.raw6622step0 line 457
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical6622 line 459
  103. def OAI.MUB6.Certificate.PairSemantics.raw6623 line 468
  104. def OAI.MUB6.Certificate.PairSemantics.raw6623step0 line 470
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical6623 line 472