OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionData13.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm416 line 11
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm416 line 13
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic416 line 15
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm417 line 20
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm417 line 22
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic417 line 24
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm418 line 29
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm418 line 31
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic418 line 33
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm419 line 37
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm419 line 39
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic419 line 41
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm420 line 46
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm420 line 48
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic420 line 50
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm421 line 55
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm421 line 57
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic421 line 59
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm422 line 64
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm422 line 66
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic422 line 68
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm423 line 72
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm423 line 74
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic423 line 76
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm424 line 81
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm424 line 83
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic424 line 85
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm425 line 90
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm425 line 92
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic425 line 94
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm426 line 98
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm426 line 100
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic426 line 102
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm427 line 107
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm427 line 109
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic427 line 111
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm428 line 115
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm428 line 117
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic428 line 119
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm429 line 123
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm429 line 125
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic429 line 127
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm430 line 131
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm430 line 133
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic430 line 135
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm431 line 139
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm431 line 141
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic431 line 143
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm432 line 147
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm432 line 149
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic432 line 151
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm433 line 155
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm433 line 157
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic433 line 159
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm434 line 163
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm434 line 165
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic434 line 167
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm435 line 171
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm435 line 173
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic435 line 175
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm436 line 179
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm436 line 181
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic436 line 183
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm437 line 187
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm437 line 189
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic437 line 191
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm438 line 195
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm438 line 197
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic438 line 199
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm439 line 203
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm439 line 205
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic439 line 207
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm440 line 211
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm440 line 213
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic440 line 215
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm441 line 219
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm441 line 221
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic441 line 223
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm442 line 227
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm442 line 229
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic442 line 231
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm443 line 235
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm443 line 237
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic443 line 239
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm444 line 243
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm444 line 245
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic444 line 247
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm445 line 251
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm445 line 253
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic445 line 255
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm446 line 259
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm446 line 261
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic446 line 263
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm447 line 267
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm447 line 269
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic447 line 271