OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionData24.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm768 line 12
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm768 line 14
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic768 line 16
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm769 line 20
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm769 line 22
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic769 line 24
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm770 line 28
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm770 line 30
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic770 line 32
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm771 line 36
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm771 line 38
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic771 line 40
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm772 line 44
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm772 line 46
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic772 line 48
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm773 line 52
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm773 line 54
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic773 line 56
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm774 line 60
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm774 line 62
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic774 line 64
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm775 line 68
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm775 line 70
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic775 line 72
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm776 line 76
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm776 line 78
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic776 line 80
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm777 line 84
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm777 line 86
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic777 line 88
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm778 line 92
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm778 line 94
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic778 line 96
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm779 line 100
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm779 line 102
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic779 line 104
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm780 line 108
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm780 line 110
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic780 line 112
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm781 line 116
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm781 line 118
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic781 line 120
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm782 line 124
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm782 line 126
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic782 line 128
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm783 line 132
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm783 line 134
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic783 line 136
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm784 line 140
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm784 line 142
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic784 line 144
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm785 line 148
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm785 line 150
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic785 line 152
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm786 line 156
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm786 line 158
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic786 line 160
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm787 line 164
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm787 line 166
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic787 line 168
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm788 line 172
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm788 line 174
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic788 line 176
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm789 line 180
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm789 line 182
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic789 line 184
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm790 line 188
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm790 line 190
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic790 line 192
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm791 line 196
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm791 line 198
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic791 line 200
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm792 line 204
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm792 line 206
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic792 line 208
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm793 line 212
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm793 line 214
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic793 line 216
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm794 line 220
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm794 line 222
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic794 line 224
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm795 line 228
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm795 line 230
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic795 line 232
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm796 line 236
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm796 line 238
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic796 line 240
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm797 line 244
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm797 line 246
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic797 line 248
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm798 line 252
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm798 line 254
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic798 line 256
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm799 line 260
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm799 line 262
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic799 line 264