OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic118.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1888 line 34
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1888 line 37
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1888 line 39
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1888 line 41
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1889 line 45
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1889 line 48
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1889 line 50
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1889 line 52
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1890 line 56
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1890 line 59
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1890 line 61
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1890 line 63
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1891 line 67
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1891 line 70
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1891 line 72
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1891 line 74
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1892 line 78
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1892 line 81
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1892 line 83
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1892 line 85
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1893 line 89
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1893 line 92
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1893 line 94
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1893 line 96
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1894 line 100
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1894 line 103
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1894 line 105
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1894 line 107
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1895 line 111
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1895 line 114
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1895 line 116
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1895 line 118
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1896 line 122
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1896 line 125
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1896 line 127
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1896 line 129
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1897 line 133
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1897 line 136
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1897 line 138
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1897 line 140
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1898 line 144
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1898 line 147
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1898 line 149
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1898 line 151
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1899 line 155
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1899 line 158
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1899 line 160
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1899 line 162
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1900 line 166
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1900 line 169
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1900 line 171
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1900 line 173
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1901 line 177
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1901 line 180
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1901 line 182
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1901 line 184
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1902 line 188
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1902 line 191
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1902 line 193
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1902 line 195
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1903 line 199
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1903 line 202
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1903 line 204
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1903 line 206