OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionData11.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm352 line 11
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm352 line 13
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic352 line 15
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm353 line 20
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm353 line 22
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic353 line 24
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm354 line 29
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm354 line 31
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic354 line 33
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm355 line 38
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm355 line 40
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic355 line 42
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm356 line 47
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm356 line 49
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic356 line 51
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm357 line 56
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm357 line 58
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic357 line 60
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm358 line 65
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm358 line 67
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic358 line 69
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm359 line 74
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm359 line 76
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic359 line 78
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm360 line 83
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm360 line 85
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic360 line 87
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm361 line 92
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm361 line 94
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic361 line 96
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm362 line 101
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm362 line 103
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic362 line 105
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm363 line 110
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm363 line 112
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic363 line 114
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm364 line 119
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm364 line 121
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic364 line 123
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm365 line 128
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm365 line 130
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic365 line 132
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm366 line 136
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm366 line 138
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic366 line 140
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm367 line 144
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm367 line 146
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic367 line 148
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm368 line 152
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm368 line 154
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic368 line 156
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm369 line 161
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm369 line 163
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic369 line 165
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm370 line 170
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm370 line 172
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic370 line 174
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm371 line 178
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm371 line 180
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic371 line 182
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm372 line 187
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm372 line 189
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic372 line 191
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm373 line 196
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm373 line 198
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic373 line 200
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm374 line 205
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm374 line 207
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic374 line 209
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm375 line 214
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm375 line 216
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic375 line 218
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm376 line 223
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm376 line 225
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic376 line 227
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm377 line 232
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm377 line 234
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic377 line 236
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm378 line 241
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm378 line 243
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic378 line 245
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm379 line 250
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm379 line 252
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic379 line 254
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm380 line 259
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm380 line 261
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic380 line 263
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm381 line 267
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm381 line 269
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic381 line 271
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm382 line 276
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm382 line 278
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic382 line 280
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm383 line 285
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm383 line 287
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic383 line 289