OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic51.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource816 line 41
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow816 line 44
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck816 line 46
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck816 line 48
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource817 line 53
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow817 line 56
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck817 line 58
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck817 line 60
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource818 line 65
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow818 line 68
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck818 line 70
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck818 line 72
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource819 line 77
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow819 line 80
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck819 line 82
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck819 line 84
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource820 line 88
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow820 line 91
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck820 line 93
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck820 line 95
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource821 line 99
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow821 line 102
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck821 line 104
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck821 line 106
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource822 line 111
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow822 line 114
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck822 line 116
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck822 line 118
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource823 line 123
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow823 line 126
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck823 line 128
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck823 line 130
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource824 line 135
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow824 line 138
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck824 line 140
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck824 line 142
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource825 line 146
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow825 line 149
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck825 line 151
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck825 line 153
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource826 line 157
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow826 line 160
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck826 line 162
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck826 line 164
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource827 line 168
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow827 line 171
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck827 line 173
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck827 line 175
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource828 line 179
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow828 line 182
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck828 line 184
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck828 line 186
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource829 line 190
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow829 line 193
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck829 line 195
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck829 line 197
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource830 line 201
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow830 line 204
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck830 line 206
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck830 line 208
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource831 line 212
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow831 line 215
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck831 line 217
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck831 line 219