OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionData51.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1632 line 12
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1632 line 14
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1632 line 16
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1633 line 20
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1633 line 22
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1633 line 24
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1634 line 28
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1634 line 30
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1634 line 32
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1635 line 36
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1635 line 38
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1635 line 40
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1636 line 44
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1636 line 46
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1636 line 48
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1637 line 52
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1637 line 54
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1637 line 56
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1638 line 60
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1638 line 62
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1638 line 64
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1639 line 68
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1639 line 70
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1639 line 72
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1640 line 76
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1640 line 78
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1640 line 80
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1641 line 84
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1641 line 86
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1641 line 88
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1642 line 92
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1642 line 94
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1642 line 96
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1643 line 100
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1643 line 102
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1643 line 104
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1644 line 108
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1644 line 110
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1644 line 112
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1645 line 116
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1645 line 118
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1645 line 120
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1646 line 124
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1646 line 126
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1646 line 128
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1647 line 132
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1647 line 134
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1647 line 136
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1648 line 140
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1648 line 142
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1648 line 144
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1649 line 148
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1649 line 150
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1649 line 152
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1650 line 156
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1650 line 158
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1650 line 160
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1651 line 164
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1651 line 166
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1651 line 168
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1652 line 172
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1652 line 174
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1652 line 176
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1653 line 180
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1653 line 182
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1653 line 184
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1654 line 188
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1654 line 190
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1654 line 192
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1655 line 196
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1655 line 198
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1655 line 200
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1656 line 204
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1656 line 206
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1656 line 208
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1657 line 212
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1657 line 214
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1657 line 216
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1658 line 220
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1658 line 222
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1658 line 224
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1659 line 228
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1659 line 230
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1659 line 232
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1660 line 236
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1660 line 238
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1660 line 240
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1661 line 244
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1661 line 246
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1661 line 248
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1662 line 252
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1662 line 254
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1662 line 256
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1663 line 260
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1663 line 262
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1663 line 264