OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionData12.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm384 line 11
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm384 line 13
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic384 line 15
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm385 line 20
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm385 line 22
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic385 line 24
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm386 line 29
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm386 line 31
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic386 line 33
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm387 line 38
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm387 line 40
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic387 line 42
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm388 line 47
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm388 line 49
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic388 line 51
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm389 line 56
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm389 line 58
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic389 line 60
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm390 line 65
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm390 line 67
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic390 line 69
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm391 line 74
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm391 line 76
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic391 line 78
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm392 line 83
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm392 line 85
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic392 line 87
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm393 line 92
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm393 line 94
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic393 line 96
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm394 line 100
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm394 line 102
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic394 line 104
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm395 line 109
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm395 line 111
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic395 line 113
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm396 line 118
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm396 line 120
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic396 line 122
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm397 line 127
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm397 line 129
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic397 line 131
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm398 line 136
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm398 line 138
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic398 line 140
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm399 line 145
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm399 line 147
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic399 line 149
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm400 line 154
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm400 line 156
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic400 line 158
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm401 line 163
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm401 line 165
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic401 line 167
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm402 line 172
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm402 line 174
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic402 line 176
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm403 line 181
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm403 line 183
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic403 line 185
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm404 line 190
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm404 line 192
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic404 line 194
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm405 line 198
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm405 line 200
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic405 line 202
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm406 line 207
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm406 line 209
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic406 line 211
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm407 line 216
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm407 line 218
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic407 line 220
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm408 line 225
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm408 line 227
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic408 line 229
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm409 line 234
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm409 line 236
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic409 line 238
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm410 line 242
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm410 line 244
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic410 line 246
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm411 line 251
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm411 line 253
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic411 line 255
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm412 line 260
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm412 line 262
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic412 line 264
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm413 line 268
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm413 line 270
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic413 line 272
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm414 line 277
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm414 line 279
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic414 line 281
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm415 line 286
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm415 line 288
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic415 line 290