OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic56.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource896 line 40
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow896 line 43
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck896 line 45
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck896 line 47
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource897 line 52
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow897 line 55
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck897 line 57
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck897 line 59
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource898 line 64
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow898 line 67
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck898 line 69
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck898 line 71
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource899 line 76
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow899 line 79
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck899 line 81
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck899 line 83
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource900 line 88
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow900 line 91
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck900 line 93
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck900 line 95
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource901 line 100
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow901 line 103
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck901 line 105
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck901 line 107
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource902 line 112
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow902 line 115
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck902 line 117
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck902 line 119
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource903 line 124
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow903 line 127
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck903 line 129
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck903 line 131
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource904 line 136
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow904 line 139
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck904 line 141
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck904 line 143
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource905 line 148
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow905 line 151
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck905 line 153
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck905 line 155
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource906 line 160
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow906 line 163
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck906 line 165
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck906 line 167
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource907 line 172
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow907 line 175
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck907 line 177
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck907 line 179
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource908 line 183
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow908 line 186
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck908 line 188
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck908 line 190
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource909 line 195
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow909 line 198
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck909 line 200
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck909 line 202
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource910 line 207
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow910 line 210
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck910 line 212
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck910 line 214
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource911 line 219
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow911 line 222
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck911 line 224
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck911 line 226