OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic7.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource112 line 46
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow112 line 49
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck112 line 51
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck112 line 53
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource113 line 57
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow113 line 60
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck113 line 62
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck113 line 64
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource114 line 68
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow114 line 71
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck114 line 73
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck114 line 75
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource115 line 79
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow115 line 82
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck115 line 84
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck115 line 86
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource116 line 90
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow116 line 93
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck116 line 95
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck116 line 97
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource117 line 101
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow117 line 104
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck117 line 106
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck117 line 108
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource118 line 112
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow118 line 115
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck118 line 117
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck118 line 119
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource119 line 123
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow119 line 126
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck119 line 128
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck119 line 130
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource120 line 134
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow120 line 137
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck120 line 139
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck120 line 141
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource121 line 145
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow121 line 148
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck121 line 150
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck121 line 152
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource122 line 156
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow122 line 159
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck122 line 161
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck122 line 163
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource123 line 167
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow123 line 170
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck123 line 172
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck123 line 174
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource124 line 178
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow124 line 181
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck124 line 183
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck124 line 185
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource125 line 189
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow125 line 192
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck125 line 194
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck125 line 196
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource126 line 200
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow126 line 203
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck126 line 205
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck126 line 207
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource127 line 211
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow127 line 214
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck127 line 216
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck127 line 218