OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic50.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource800 line 45
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow800 line 48
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck800 line 50
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck800 line 52
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource801 line 56
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow801 line 59
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck801 line 61
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck801 line 63
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource802 line 67
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow802 line 70
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck802 line 72
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck802 line 74
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource803 line 78
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow803 line 81
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck803 line 83
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck803 line 85
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource804 line 89
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow804 line 92
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck804 line 94
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck804 line 96
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource805 line 100
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow805 line 103
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck805 line 105
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck805 line 107
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource806 line 111
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow806 line 114
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck806 line 116
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck806 line 118
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource807 line 122
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow807 line 125
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck807 line 127
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck807 line 129
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource808 line 133
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow808 line 136
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck808 line 138
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck808 line 140
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource809 line 144
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow809 line 147
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck809 line 149
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck809 line 151
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource810 line 155
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow810 line 158
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck810 line 160
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck810 line 162
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource811 line 166
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow811 line 169
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck811 line 171
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck811 line 173
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource812 line 177
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow812 line 180
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck812 line 182
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck812 line 184
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource813 line 188
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow813 line 191
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck813 line 193
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck813 line 195
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource814 line 199
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow814 line 202
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck814 line 204
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck814 line 206
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource815 line 210
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow815 line 213
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck815 line 215
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck815 line 217