OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic1.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource16 line 26
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow16 line 29
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck16 line 31
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck16 line 33
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource17 line 38
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow17 line 41
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck17 line 43
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck17 line 45
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource18 line 50
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow18 line 53
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck18 line 55
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck18 line 57
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource19 line 62
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow19 line 65
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck19 line 67
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck19 line 69
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource20 line 74
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow20 line 77
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck20 line 79
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck20 line 81
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource21 line 86
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow21 line 89
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck21 line 91
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck21 line 93
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource22 line 98
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow22 line 101
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck22 line 103
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck22 line 105
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource23 line 110
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow23 line 113
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck23 line 115
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck23 line 117
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource24 line 122
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow24 line 125
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck24 line 127
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck24 line 129
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource25 line 134
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow25 line 137
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck25 line 139
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck25 line 141
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource26 line 146
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow26 line 149
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck26 line 151
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck26 line 153
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource27 line 158
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow27 line 161
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck27 line 163
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck27 line 165
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource28 line 170
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow28 line 173
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck28 line 175
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck28 line 177
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource29 line 182
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow29 line 185
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck29 line 187
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck29 line 189
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource30 line 194
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow30 line 197
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck30 line 199
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck30 line 201
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource31 line 205
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow31 line 208
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck31 line 210
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck31 line 212