OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic127.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2032 line 51
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2032 line 54
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2032 line 56
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2032 line 58
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2033 line 62
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2033 line 65
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2033 line 67
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2033 line 69
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2034 line 73
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2034 line 76
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2034 line 78
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2034 line 80
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2035 line 84
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2035 line 87
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2035 line 89
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2035 line 91
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2036 line 95
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2036 line 98
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2036 line 100
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2036 line 102
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2037 line 106
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2037 line 109
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2037 line 111
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2037 line 113
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2038 line 117
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2038 line 120
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2038 line 122
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2038 line 124
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2039 line 128
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2039 line 131
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2039 line 133
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2039 line 135
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2040 line 139
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2040 line 142
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2040 line 144
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2040 line 146
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2041 line 150
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2041 line 153
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2041 line 155
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2041 line 157
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2042 line 161
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2042 line 164
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2042 line 166
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2042 line 168
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2043 line 172
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2043 line 175
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2043 line 177
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2043 line 179
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2044 line 183
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2044 line 186
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2044 line 188
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2044 line 190
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2045 line 194
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2045 line 197
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2045 line 199
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2045 line 201
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2046 line 205
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2046 line 208
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2046 line 210
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2046 line 212
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2047 line 216
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2047 line 219
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2047 line 221
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2047 line 223