OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic29.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource464 line 43
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow464 line 46
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck464 line 48
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck464 line 50
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource465 line 54
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow465 line 57
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck465 line 59
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck465 line 61
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource466 line 65
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow466 line 68
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck466 line 70
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck466 line 72
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource467 line 76
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow467 line 79
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck467 line 81
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck467 line 83
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource468 line 87
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow468 line 90
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck468 line 92
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck468 line 94
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource469 line 98
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow469 line 101
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck469 line 103
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck469 line 105
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource470 line 109
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow470 line 112
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck470 line 114
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck470 line 116
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource471 line 121
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow471 line 124
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck471 line 126
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck471 line 128
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource472 line 132
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow472 line 135
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck472 line 137
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck472 line 139
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource473 line 143
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow473 line 146
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck473 line 148
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck473 line 150
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource474 line 155
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow474 line 158
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck474 line 160
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck474 line 162
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource475 line 167
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow475 line 170
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck475 line 172
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck475 line 174
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource476 line 179
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow476 line 182
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck476 line 184
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck476 line 186
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource477 line 190
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow477 line 193
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck477 line 195
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck477 line 197
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource478 line 201
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow478 line 204
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck478 line 206
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck478 line 208
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource479 line 212
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow479 line 215
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck479 line 217
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck479 line 219