OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic116.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1856 line 54
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1856 line 57
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1856 line 59
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1856 line 61
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1857 line 66
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1857 line 69
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1857 line 71
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1857 line 73
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1858 line 77
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1858 line 80
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1858 line 82
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1858 line 84
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1859 line 89
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1859 line 92
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1859 line 94
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1859 line 96
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1860 line 101
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1860 line 104
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1860 line 106
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1860 line 108
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1861 line 112
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1861 line 115
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1861 line 117
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1861 line 119
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1862 line 123
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1862 line 126
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1862 line 128
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1862 line 130
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1863 line 134
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1863 line 137
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1863 line 139
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1863 line 141
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1864 line 145
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1864 line 148
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1864 line 150
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1864 line 152
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1865 line 157
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1865 line 160
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1865 line 162
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1865 line 164
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1866 line 169
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1866 line 172
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1866 line 174
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1866 line 176
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1867 line 181
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1867 line 184
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1867 line 186
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1867 line 188
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1868 line 192
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1868 line 195
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1868 line 197
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1868 line 199
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1869 line 203
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1869 line 206
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1869 line 208
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1869 line 210
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1870 line 214
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1870 line 217
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1870 line 219
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1870 line 221
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1871 line 225
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1871 line 228
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1871 line 230
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1871 line 232