OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic81.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1296 line 51
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1296 line 54
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1296 line 56
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1296 line 58
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1297 line 62
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1297 line 65
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1297 line 67
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1297 line 69
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1298 line 73
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1298 line 76
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1298 line 78
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1298 line 80
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1299 line 84
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1299 line 87
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1299 line 89
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1299 line 91
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1300 line 95
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1300 line 98
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1300 line 100
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1300 line 102
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1301 line 106
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1301 line 109
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1301 line 111
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1301 line 113
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1302 line 117
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1302 line 120
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1302 line 122
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1302 line 124
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1303 line 128
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1303 line 131
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1303 line 133
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1303 line 135
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1304 line 139
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1304 line 142
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1304 line 144
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1304 line 146
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1305 line 150
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1305 line 153
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1305 line 155
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1305 line 157
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1306 line 161
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1306 line 164
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1306 line 166
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1306 line 168
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1307 line 172
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1307 line 175
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1307 line 177
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1307 line 179
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1308 line 183
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1308 line 186
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1308 line 188
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1308 line 190
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1309 line 194
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1309 line 197
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1309 line 199
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1309 line 201
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1310 line 205
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1310 line 208
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1310 line 210
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1310 line 212
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1311 line 216
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1311 line 219
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1311 line 221
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1311 line 223