OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic73.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1168 line 54
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1168 line 57
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1168 line 59
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1168 line 61
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1169 line 65
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1169 line 68
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1169 line 70
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1169 line 72
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1170 line 77
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1170 line 80
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1170 line 82
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1170 line 84
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1171 line 89
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1171 line 92
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1171 line 94
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1171 line 96
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1172 line 100
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1172 line 103
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1172 line 105
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1172 line 107
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1173 line 111
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1173 line 114
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1173 line 116
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1173 line 118
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1174 line 122
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1174 line 125
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1174 line 127
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1174 line 129
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1175 line 133
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1175 line 136
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1175 line 138
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1175 line 140
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1176 line 144
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1176 line 147
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1176 line 149
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1176 line 151
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1177 line 155
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1177 line 158
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1177 line 160
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1177 line 162
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1178 line 167
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1178 line 170
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1178 line 172
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1178 line 174
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1179 line 179
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1179 line 182
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1179 line 184
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1179 line 186
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1180 line 191
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1180 line 194
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1180 line 196
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1180 line 198
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1181 line 202
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1181 line 205
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1181 line 207
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1181 line 209
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1182 line 213
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1182 line 216
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1182 line 218
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1182 line 220
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1183 line 224
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1183 line 227
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1183 line 229
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1183 line 231