OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical284.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9088 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw9088step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw9088step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical9088 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw9089 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw9089step0 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw9089step1 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw9089step2 line 45
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9089 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw9090 line 64
  11. def OAI.MUB6.Certificate.PairSemantics.raw9090step0 line 66
  12. def OAI.MUB6.Certificate.PairSemantics.raw9090step1 line 68
  13. def OAI.MUB6.Certificate.PairSemantics.raw9090step2 line 70
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical9090 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw9091 line 89
  16. def OAI.MUB6.Certificate.PairSemantics.raw9091step0 line 91
  17. def OAI.MUB6.Certificate.PairSemantics.raw9091step1 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw9091step2 line 95
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9091 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw9092 line 114
  21. def OAI.MUB6.Certificate.PairSemantics.raw9092step0 line 116
  22. def OAI.MUB6.Certificate.PairSemantics.raw9092step1 line 118
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical9092 line 120
  24. def OAI.MUB6.Certificate.PairSemantics.raw9093 line 133
  25. def OAI.MUB6.Certificate.PairSemantics.raw9093step0 line 135
  26. def OAI.MUB6.Certificate.PairSemantics.raw9093step1 line 137
  27. def OAI.MUB6.Certificate.PairSemantics.raw9093step2 line 139
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical9093 line 141
  29. def OAI.MUB6.Certificate.PairSemantics.raw9094 line 158
  30. def OAI.MUB6.Certificate.PairSemantics.raw9094step0 line 160
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical9094 line 162
  32. def OAI.MUB6.Certificate.PairSemantics.raw9095 line 171
  33. def OAI.MUB6.Certificate.PairSemantics.raw9095step0 line 173
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical9095 line 175
  35. def OAI.MUB6.Certificate.PairSemantics.raw9096 line 184
  36. def OAI.MUB6.Certificate.PairSemantics.raw9096step0 line 186
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical9096 line 188
  38. def OAI.MUB6.Certificate.PairSemantics.raw9097 line 197
  39. def OAI.MUB6.Certificate.PairSemantics.raw9097step0 line 199
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical9097 line 201
  41. def OAI.MUB6.Certificate.PairSemantics.raw9098 line 210
  42. def OAI.MUB6.Certificate.PairSemantics.raw9098step0 line 212
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical9098 line 214
  44. def OAI.MUB6.Certificate.PairSemantics.raw9099 line 223
  45. def OAI.MUB6.Certificate.PairSemantics.raw9099step0 line 225
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical9099 line 227
  47. def OAI.MUB6.Certificate.PairSemantics.raw9100 line 236
  48. def OAI.MUB6.Certificate.PairSemantics.raw9100step0 line 238
  49. def OAI.MUB6.Certificate.PairSemantics.raw9100step1 line 240
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9100 line 242
  51. def OAI.MUB6.Certificate.PairSemantics.raw9101 line 256
  52. def OAI.MUB6.Certificate.PairSemantics.raw9101step0 line 258
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9101 line 260
  54. def OAI.MUB6.Certificate.PairSemantics.raw9102 line 269
  55. def OAI.MUB6.Certificate.PairSemantics.raw9102step0 line 271
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical9102 line 273
  57. def OAI.MUB6.Certificate.PairSemantics.raw9103 line 282
  58. def OAI.MUB6.Certificate.PairSemantics.raw9103step0 line 284
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9103 line 286
  60. def OAI.MUB6.Certificate.PairSemantics.raw9104 line 295
  61. def OAI.MUB6.Certificate.PairSemantics.raw9104step0 line 297
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical9104 line 299
  63. def OAI.MUB6.Certificate.PairSemantics.raw9105 line 308
  64. def OAI.MUB6.Certificate.PairSemantics.raw9105step0 line 310
  65. def OAI.MUB6.Certificate.PairSemantics.raw9105step1 line 312
  66. def OAI.MUB6.Certificate.PairSemantics.raw9105step2 line 314
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical9105 line 316
  68. def OAI.MUB6.Certificate.PairSemantics.raw9106 line 334
  69. def OAI.MUB6.Certificate.PairSemantics.raw9106step0 line 336
  70. def OAI.MUB6.Certificate.PairSemantics.raw9106step1 line 338
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical9106 line 340
  72. def OAI.MUB6.Certificate.PairSemantics.raw9107 line 353
  73. def OAI.MUB6.Certificate.PairSemantics.raw9107step0 line 355
  74. def OAI.MUB6.Certificate.PairSemantics.raw9107step1 line 357
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical9107 line 359
  76. def OAI.MUB6.Certificate.PairSemantics.raw9108 line 372
  77. def OAI.MUB6.Certificate.PairSemantics.raw9108step0 line 374
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9108 line 376
  79. def OAI.MUB6.Certificate.PairSemantics.raw9109 line 385
  80. def OAI.MUB6.Certificate.PairSemantics.raw9109step0 line 387
  81. def OAI.MUB6.Certificate.PairSemantics.raw9109step1 line 389
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical9109 line 391
  83. def OAI.MUB6.Certificate.PairSemantics.raw9110 line 404
  84. def OAI.MUB6.Certificate.PairSemantics.raw9110step0 line 406
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical9110 line 408
  86. def OAI.MUB6.Certificate.PairSemantics.raw9111 line 417
  87. def OAI.MUB6.Certificate.PairSemantics.raw9111step0 line 419
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical9111 line 421
  89. def OAI.MUB6.Certificate.PairSemantics.raw9112 line 430
  90. def OAI.MUB6.Certificate.PairSemantics.raw9112step0 line 432
  91. def OAI.MUB6.Certificate.PairSemantics.raw9112step1 line 434
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9112 line 436
  93. def OAI.MUB6.Certificate.PairSemantics.raw9113 line 449
  94. def OAI.MUB6.Certificate.PairSemantics.raw9113step0 line 451
  95. def OAI.MUB6.Certificate.PairSemantics.raw9113step1 line 453
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical9113 line 455
  97. def OAI.MUB6.Certificate.PairSemantics.raw9114 line 468
  98. def OAI.MUB6.Certificate.PairSemantics.raw9114step0 line 470
  99. def OAI.MUB6.Certificate.PairSemantics.raw9114step1 line 472
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical9114 line 474
  101. def OAI.MUB6.Certificate.PairSemantics.raw9115 line 487
  102. def OAI.MUB6.Certificate.PairSemantics.raw9115step0 line 489
  103. def OAI.MUB6.Certificate.PairSemantics.raw9115step1 line 491
  104. def OAI.MUB6.Certificate.PairSemantics.raw9115step2 line 493
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical9115 line 495
  106. def OAI.MUB6.Certificate.PairSemantics.raw9116 line 515
  107. def OAI.MUB6.Certificate.PairSemantics.raw9116step0 line 517
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical9116 line 519
  109. def OAI.MUB6.Certificate.PairSemantics.raw9117 line 528
  110. def OAI.MUB6.Certificate.PairSemantics.raw9117step0 line 530
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical9117 line 532
  112. def OAI.MUB6.Certificate.PairSemantics.raw9118 line 541
  113. def OAI.MUB6.Certificate.PairSemantics.raw9118step0 line 543
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical9118 line 545
  115. def OAI.MUB6.Certificate.PairSemantics.raw9119 line 554
  116. def OAI.MUB6.Certificate.PairSemantics.raw9119step0 line 556
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical9119 line 558