OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic123.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1968 line 58
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1968 line 61
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1968 line 63
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1968 line 65
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1969 line 70
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1969 line 73
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1969 line 75
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1969 line 77
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1970 line 82
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1970 line 85
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1970 line 87
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1970 line 89
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1971 line 94
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1971 line 97
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1971 line 99
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1971 line 101
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1972 line 106
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1972 line 109
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1972 line 111
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1972 line 113
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1973 line 118
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1973 line 121
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1973 line 123
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1973 line 125
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1974 line 129
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1974 line 132
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1974 line 134
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1974 line 136
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1975 line 140
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1975 line 143
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1975 line 145
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1975 line 147
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1976 line 151
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1976 line 154
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1976 line 156
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1976 line 158
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1977 line 163
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1977 line 166
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1977 line 168
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1977 line 170
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1978 line 175
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1978 line 178
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1978 line 180
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1978 line 182
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1979 line 187
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1979 line 190
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1979 line 192
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1979 line 194
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1980 line 198
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1980 line 201
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1980 line 203
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1980 line 205
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1981 line 210
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1981 line 213
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1981 line 215
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1981 line 217
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1982 line 221
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1982 line 224
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1982 line 226
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1982 line 228
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1983 line 232
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1983 line 235
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1983 line 237
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1983 line 239