OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic19.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource304 line 37
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow304 line 40
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck304 line 42
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck304 line 44
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource305 line 48
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow305 line 51
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck305 line 53
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck305 line 55
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource306 line 59
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow306 line 62
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck306 line 64
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck306 line 66
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource307 line 70
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow307 line 73
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck307 line 75
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck307 line 77
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource308 line 81
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow308 line 84
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck308 line 86
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck308 line 88
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource309 line 92
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow309 line 95
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck309 line 97
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck309 line 99
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource310 line 104
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow310 line 107
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck310 line 109
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck310 line 111
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource311 line 116
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow311 line 119
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck311 line 121
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck311 line 123
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource312 line 128
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow312 line 131
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck312 line 133
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck312 line 135
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource313 line 139
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow313 line 142
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck313 line 144
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck313 line 146
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource314 line 150
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow314 line 153
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck314 line 155
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck314 line 157
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource315 line 161
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow315 line 164
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck315 line 166
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck315 line 168
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource316 line 172
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow316 line 175
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck316 line 177
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck316 line 179
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource317 line 183
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow317 line 186
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck317 line 188
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck317 line 190
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource318 line 194
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow318 line 197
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck318 line 199
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck318 line 201
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource319 line 205
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow319 line 208
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck319 line 210
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck319 line 212