OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic119.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1904 line 58
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1904 line 61
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1904 line 63
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1904 line 65
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1905 line 70
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1905 line 73
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1905 line 75
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1905 line 77
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1906 line 82
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1906 line 85
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1906 line 87
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1906 line 89
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1907 line 94
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1907 line 97
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1907 line 99
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1907 line 101
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1908 line 106
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1908 line 109
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1908 line 111
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1908 line 113
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1909 line 118
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1909 line 121
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1909 line 123
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1909 line 125
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1910 line 130
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1910 line 133
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1910 line 135
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1910 line 137
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1911 line 142
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1911 line 145
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1911 line 147
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1911 line 149
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1912 line 154
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1912 line 157
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1912 line 159
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1912 line 161
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1913 line 166
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1913 line 169
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1913 line 171
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1913 line 173
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1914 line 177
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1914 line 180
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1914 line 182
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1914 line 184
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1915 line 189
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1915 line 192
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1915 line 194
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1915 line 196
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1916 line 201
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1916 line 204
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1916 line 206
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1916 line 208
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1917 line 213
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1917 line 216
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1917 line 218
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1917 line 220
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1918 line 225
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1918 line 228
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1918 line 230
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1918 line 232
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1919 line 237
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1919 line 240
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1919 line 242
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1919 line 244