OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic11.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource176 line 40
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow176 line 43
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck176 line 45
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck176 line 47
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource177 line 52
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow177 line 55
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck177 line 57
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck177 line 59
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource178 line 63
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow178 line 66
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck178 line 68
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck178 line 70
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource179 line 74
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow179 line 77
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck179 line 79
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck179 line 81
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource180 line 85
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow180 line 88
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck180 line 90
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck180 line 92
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource181 line 96
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow181 line 99
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck181 line 101
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck181 line 103
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource182 line 107
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow182 line 110
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck182 line 112
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck182 line 114
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource183 line 118
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow183 line 121
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck183 line 123
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck183 line 125
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource184 line 129
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow184 line 132
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck184 line 134
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck184 line 136
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource185 line 141
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow185 line 144
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck185 line 146
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck185 line 148
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource186 line 152
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow186 line 155
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck186 line 157
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck186 line 159
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource187 line 163
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow187 line 166
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck187 line 168
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck187 line 170
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource188 line 174
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow188 line 177
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck188 line 179
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck188 line 181
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource189 line 186
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow189 line 189
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck189 line 191
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck189 line 193
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource190 line 197
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow190 line 200
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck190 line 202
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck190 line 204
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource191 line 208
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow191 line 211
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck191 line 213
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck191 line 215