OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic133.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2128 line 23
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2128 line 26
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2128 line 28
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2128 line 30
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2129 line 34
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2129 line 37
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2129 line 39
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2129 line 41
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2130 line 45
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2130 line 48
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2130 line 50
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2130 line 52
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2131 line 56
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2131 line 59
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2131 line 61
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2131 line 63
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2132 line 67
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2132 line 70
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2132 line 72
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2132 line 74
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2133 line 78
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2133 line 81
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2133 line 83
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2133 line 85
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2134 line 89
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2134 line 92
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2134 line 94
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2134 line 96
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2135 line 100
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2135 line 103
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2135 line 105
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2135 line 107
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2136 line 111
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2136 line 114
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2136 line 116
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2136 line 118
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2137 line 122
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2137 line 125
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2137 line 127
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2137 line 129
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2138 line 133
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2138 line 136
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2138 line 138
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2138 line 140
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2139 line 144
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2139 line 147
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2139 line 149
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2139 line 151
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2140 line 155
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2140 line 158
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2140 line 160
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2140 line 162
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2141 line 166
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2141 line 169
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2141 line 171
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2141 line 173
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2142 line 177
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2142 line 180
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2142 line 182
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2142 line 184
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2143 line 188
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2143 line 191
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2143 line 193
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2143 line 195