OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic72.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1152 line 49
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1152 line 52
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1152 line 54
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1152 line 56
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1153 line 60
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1153 line 63
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1153 line 65
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1153 line 67
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1154 line 71
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1154 line 74
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1154 line 76
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1154 line 78
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1155 line 82
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1155 line 85
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1155 line 87
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1155 line 89
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1156 line 93
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1156 line 96
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1156 line 98
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1156 line 100
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1157 line 104
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1157 line 107
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1157 line 109
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1157 line 111
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1158 line 115
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1158 line 118
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1158 line 120
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1158 line 122
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1159 line 127
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1159 line 130
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1159 line 132
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1159 line 134
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1160 line 139
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1160 line 142
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1160 line 144
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1160 line 146
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1161 line 150
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1161 line 153
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1161 line 155
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1161 line 157
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1162 line 161
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1162 line 164
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1162 line 166
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1162 line 168
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1163 line 172
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1163 line 175
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1163 line 177
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1163 line 179
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1164 line 183
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1164 line 186
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1164 line 188
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1164 line 190
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1165 line 194
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1165 line 197
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1165 line 199
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1165 line 201
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1166 line 206
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1166 line 209
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1166 line 211
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1166 line 213
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1167 line 218
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1167 line 221
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1167 line 223
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1167 line 225