OAI/Analysis/MutuallyUnbiased/PairPolynomial/Terms.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial line 10
  2. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge0_0 line 13
  3. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge0_1 line 16
  4. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial0 line 19
  5. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge1_0 line 30
  6. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge1_1 line 33
  7. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge1_2 line 36
  8. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial1 line 39
  9. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge2_0 line 50
  10. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge2_1 line 53
  11. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge2_2 line 56
  12. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial2 line 59
  13. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge3_0 line 70
  14. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge3_1 line 73
  15. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge3_2 line 76
  16. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial3 line 79
  17. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge4_0 line 90
  18. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge4_1 line 93
  19. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge4_2 line 96
  20. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial4 line 99
  21. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge5_0 line 110
  22. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge5_1 line 113
  23. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge5_2 line 116
  24. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial5 line 119
  25. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge6_0 line 130
  26. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge6_1 line 133
  27. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge6_2 line 136
  28. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge6_3 line 139
  29. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial6 line 142
  30. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge7_0 line 153
  31. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge7_1 line 156
  32. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge7_2 line 159
  33. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge7_3 line 162
  34. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial7 line 165
  35. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge8_0 line 176
  36. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge8_1 line 179
  37. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge8_2 line 182
  38. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge8_3 line 185
  39. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial8 line 188
  40. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge9_0 line 199
  41. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge9_1 line 202
  42. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge9_2 line 205
  43. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge9_3 line 208
  44. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial9 line 211
  45. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge10_0 line 222
  46. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge10_1 line 225
  47. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge10_2 line 228
  48. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial10 line 231
  49. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge11_0 line 242
  50. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge11_1 line 245
  51. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge11_2 line 248
  52. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge11_3 line 251
  53. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial11 line 254
  54. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge12_0 line 265
  55. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge12_1 line 268
  56. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge12_2 line 271
  57. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge12_3 line 274
  58. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial12 line 277
  59. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge13_0 line 288
  60. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge13_1 line 291
  61. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge13_2 line 294
  62. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge13_3 line 297
  63. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial13 line 300
  64. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge14_0 line 311
  65. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge14_1 line 314
  66. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge14_2 line 317
  67. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge14_3 line 320
  68. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial14 line 323
  69. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge15_0 line 334
  70. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge15_1 line 337
  71. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge15_2 line 340
  72. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial15 line 343
  73. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge16_0 line 354
  74. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge16_1 line 357
  75. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge16_2 line 360
  76. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge16_3 line 363
  77. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial16 line 366
  78. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge17_0 line 377
  79. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge17_1 line 380
  80. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge17_2 line 383
  81. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge17_3 line 386
  82. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial17 line 389
  83. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge18_0 line 400
  84. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge18_1 line 403
  85. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge18_2 line 406
  86. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge18_3 line 409
  87. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial18 line 412
  88. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge19_0 line 423
  89. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge19_1 line 426
  90. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge19_2 line 429
  91. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge19_3 line 432
  92. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial19 line 435
  93. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge20_0 line 446
  94. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge20_1 line 449
  95. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge20_2 line 452
  96. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial20 line 455
  97. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge21_0 line 466
  98. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge21_1 line 469
  99. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge21_2 line 472
  100. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge21_3 line 475
  101. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial21 line 478
  102. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge22_0 line 489
  103. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge22_1 line 492
  104. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge22_2 line 495
  105. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge22_3 line 498
  106. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial22 line 501
  107. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge23_0 line 512
  108. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge23_1 line 515
  109. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge23_2 line 518
  110. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge23_3 line 521
  111. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial23 line 524
  112. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge24_0 line 535
  113. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge24_1 line 538
  114. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge24_2 line 541
  115. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge24_3 line 544
  116. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial24 line 547
  117. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge25_0 line 558
  118. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge25_1 line 561
  119. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge25_2 line 564
  120. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge25_3 line 567
  121. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial25 line 570
  122. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge26_0 line 581
  123. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge26_1 line 584
  124. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge26_2 line 587
  125. theorem OAI.MUB6.Certificate.PairTargetSemantics.charge26_3 line 590
  126. theorem OAI.MUB6.Certificate.PairTargetSemantics.termPolynomial26 line 593