OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic128.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2048 line 38
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2048 line 41
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2048 line 43
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2048 line 45
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2049 line 50
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2049 line 53
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2049 line 55
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2049 line 57
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2050 line 62
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2050 line 65
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2050 line 67
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2050 line 69
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2051 line 74
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2051 line 77
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2051 line 79
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2051 line 81
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2052 line 86
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2052 line 89
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2052 line 91
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2052 line 93
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2053 line 97
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2053 line 100
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2053 line 102
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2053 line 104
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2054 line 108
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2054 line 111
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2054 line 113
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2054 line 115
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2055 line 119
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2055 line 122
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2055 line 124
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2055 line 126
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2056 line 130
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2056 line 133
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2056 line 135
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2056 line 137
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2057 line 142
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2057 line 145
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2057 line 147
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2057 line 149
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2058 line 153
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2058 line 156
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2058 line 158
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2058 line 160
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2059 line 164
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2059 line 167
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2059 line 169
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2059 line 171
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2060 line 176
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2060 line 179
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2060 line 181
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2060 line 183
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2061 line 188
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2061 line 191
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2061 line 193
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2061 line 195
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2062 line 200
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2062 line 203
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2062 line 205
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2062 line 207
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2063 line 212
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2063 line 215
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2063 line 217
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2063 line 219