OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic82.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1312 line 47
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1312 line 50
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1312 line 52
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1312 line 54
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1313 line 59
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1313 line 62
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1313 line 64
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1313 line 66
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1314 line 70
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1314 line 73
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1314 line 75
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1314 line 77
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1315 line 81
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1315 line 84
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1315 line 86
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1315 line 88
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1316 line 92
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1316 line 95
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1316 line 97
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1316 line 99
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1317 line 103
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1317 line 106
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1317 line 108
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1317 line 110
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1318 line 115
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1318 line 118
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1318 line 120
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1318 line 122
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1319 line 127
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1319 line 130
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1319 line 132
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1319 line 134
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1320 line 138
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1320 line 141
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1320 line 143
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1320 line 145
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1321 line 149
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1321 line 152
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1321 line 154
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1321 line 156
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1322 line 161
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1322 line 164
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1322 line 166
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1322 line 168
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1323 line 172
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1323 line 175
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1323 line 177
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1323 line 179
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1324 line 183
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1324 line 186
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1324 line 188
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1324 line 190
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1325 line 195
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1325 line 198
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1325 line 200
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1325 line 202
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1326 line 206
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1326 line 209
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1326 line 211
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1326 line 213
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1327 line 218
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1327 line 221
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1327 line 223
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1327 line 225