OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic58.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource928 line 33
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow928 line 36
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck928 line 38
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck928 line 40
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource929 line 45
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow929 line 48
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck929 line 50
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck929 line 52
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource930 line 57
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow930 line 60
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck930 line 62
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck930 line 64
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource931 line 69
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow931 line 72
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck931 line 74
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck931 line 76
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource932 line 81
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow932 line 84
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck932 line 86
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck932 line 88
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource933 line 93
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow933 line 96
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck933 line 98
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck933 line 100
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource934 line 105
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow934 line 108
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck934 line 110
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck934 line 112
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource935 line 117
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow935 line 120
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck935 line 122
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck935 line 124
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource936 line 129
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow936 line 132
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck936 line 134
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck936 line 136
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource937 line 141
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow937 line 144
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck937 line 146
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck937 line 148
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource938 line 153
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow938 line 156
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck938 line 158
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck938 line 160
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource939 line 165
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow939 line 168
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck939 line 170
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck939 line 172
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource940 line 177
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow940 line 180
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck940 line 182
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck940 line 184
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource941 line 189
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow941 line 192
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck941 line 194
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck941 line 196
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource942 line 201
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow942 line 204
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck942 line 206
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck942 line 208
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource943 line 213
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow943 line 216
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck943 line 218
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck943 line 220