OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic115.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1840 line 57
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1840 line 60
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1840 line 62
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1840 line 64
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1841 line 69
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1841 line 72
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1841 line 74
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1841 line 76
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1842 line 80
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1842 line 83
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1842 line 85
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1842 line 87
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1843 line 91
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1843 line 94
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1843 line 96
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1843 line 98
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1844 line 102
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1844 line 105
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1844 line 107
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1844 line 109
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1845 line 114
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1845 line 117
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1845 line 119
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1845 line 121
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1846 line 126
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1846 line 129
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1846 line 131
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1846 line 133
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1847 line 138
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1847 line 141
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1847 line 143
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1847 line 145
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1848 line 150
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1848 line 153
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1848 line 155
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1848 line 157
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1849 line 162
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1849 line 165
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1849 line 167
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1849 line 169
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1850 line 174
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1850 line 177
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1850 line 179
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1850 line 181
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1851 line 185
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1851 line 188
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1851 line 190
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1851 line 192
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1852 line 196
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1852 line 199
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1852 line 201
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1852 line 203
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1853 line 207
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1853 line 210
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1853 line 212
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1853 line 214
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1854 line 219
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1854 line 222
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1854 line 224
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1854 line 226
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1855 line 231
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1855 line 234
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1855 line 236
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1855 line 238