OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic22.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource352 line 45
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow352 line 48
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck352 line 50
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck352 line 52
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource353 line 56
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow353 line 59
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck353 line 61
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck353 line 63
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource354 line 67
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow354 line 70
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck354 line 72
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck354 line 74
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource355 line 78
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow355 line 81
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck355 line 83
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck355 line 85
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource356 line 89
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow356 line 92
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck356 line 94
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck356 line 96
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource357 line 100
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow357 line 103
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck357 line 105
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck357 line 107
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource358 line 111
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow358 line 114
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck358 line 116
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck358 line 118
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource359 line 122
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow359 line 125
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck359 line 127
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck359 line 129
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource360 line 133
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow360 line 136
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck360 line 138
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck360 line 140
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource361 line 144
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow361 line 147
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck361 line 149
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck361 line 151
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource362 line 155
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow362 line 158
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck362 line 160
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck362 line 162
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource363 line 166
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow363 line 169
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck363 line 171
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck363 line 173
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource364 line 177
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow364 line 180
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck364 line 182
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck364 line 184
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource365 line 188
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow365 line 191
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck365 line 193
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck365 line 195
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource366 line 199
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow366 line 202
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck366 line 204
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck366 line 206
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource367 line 210
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow367 line 213
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck367 line 215
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck367 line 217