OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic17.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource272 line 46
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow272 line 49
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck272 line 51
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck272 line 53
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource273 line 57
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow273 line 60
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck273 line 62
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck273 line 64
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource274 line 68
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow274 line 71
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck274 line 73
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck274 line 75
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource275 line 79
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow275 line 82
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck275 line 84
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck275 line 86
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource276 line 90
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow276 line 93
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck276 line 95
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck276 line 97
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource277 line 101
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow277 line 104
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck277 line 106
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck277 line 108
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource278 line 112
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow278 line 115
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck278 line 117
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck278 line 119
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource279 line 123
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow279 line 126
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck279 line 128
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck279 line 130
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource280 line 134
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow280 line 137
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck280 line 139
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck280 line 141
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource281 line 145
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow281 line 148
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck281 line 150
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck281 line 152
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource282 line 157
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow282 line 160
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck282 line 162
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck282 line 164
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource283 line 169
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow283 line 172
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck283 line 174
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck283 line 176
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource284 line 180
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow284 line 183
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck284 line 185
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck284 line 187
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource285 line 191
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow285 line 194
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck285 line 196
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck285 line 198
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource286 line 202
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow286 line 205
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck286 line 207
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck286 line 209
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource287 line 214
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow287 line 217
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck287 line 219
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck287 line 221