OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic120.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1920 line 49
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1920 line 52
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1920 line 54
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1920 line 56
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1921 line 60
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1921 line 63
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1921 line 65
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1921 line 67
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1922 line 71
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1922 line 74
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1922 line 76
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1922 line 78
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1923 line 82
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1923 line 85
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1923 line 87
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1923 line 89
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1924 line 93
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1924 line 96
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1924 line 98
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1924 line 100
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1925 line 105
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1925 line 108
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1925 line 110
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1925 line 112
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1926 line 117
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1926 line 120
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1926 line 122
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1926 line 124
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1927 line 128
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1927 line 131
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1927 line 133
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1927 line 135
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1928 line 139
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1928 line 142
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1928 line 144
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1928 line 146
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1929 line 150
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1929 line 153
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1929 line 155
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1929 line 157
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1930 line 161
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1930 line 164
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1930 line 166
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1930 line 168
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1931 line 172
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1931 line 175
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1931 line 177
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1931 line 179
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1932 line 183
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1932 line 186
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1932 line 188
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1932 line 190
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1933 line 194
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1933 line 197
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1933 line 199
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1933 line 201
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1934 line 205
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1934 line 208
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1934 line 210
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1934 line 212
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1935 line 216
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1935 line 219
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1935 line 221
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1935 line 223