OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic112.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1792 line 52
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1792 line 55
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1792 line 57
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1792 line 59
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1793 line 63
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1793 line 66
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1793 line 68
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1793 line 70
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1794 line 74
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1794 line 77
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1794 line 79
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1794 line 81
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1795 line 85
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1795 line 88
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1795 line 90
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1795 line 92
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1796 line 97
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1796 line 100
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1796 line 102
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1796 line 104
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1797 line 109
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1797 line 112
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1797 line 114
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1797 line 116
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1798 line 120
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1798 line 123
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1798 line 125
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1798 line 127
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1799 line 131
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1799 line 134
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1799 line 136
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1799 line 138
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1800 line 142
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1800 line 145
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1800 line 147
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1800 line 149
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1801 line 153
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1801 line 156
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1801 line 158
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1801 line 160
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1802 line 164
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1802 line 167
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1802 line 169
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1802 line 171
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1803 line 175
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1803 line 178
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1803 line 180
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1803 line 182
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1804 line 186
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1804 line 189
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1804 line 191
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1804 line 193
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1805 line 197
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1805 line 200
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1805 line 202
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1805 line 204
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1806 line 208
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1806 line 211
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1806 line 213
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1806 line 215
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1807 line 219
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1807 line 222
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1807 line 224
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1807 line 226