OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic35.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource560 line 46
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow560 line 49
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck560 line 51
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck560 line 53
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource561 line 57
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow561 line 60
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck561 line 62
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck561 line 64
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource562 line 68
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow562 line 71
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck562 line 73
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck562 line 75
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource563 line 79
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow563 line 82
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck563 line 84
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck563 line 86
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource564 line 90
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow564 line 93
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck564 line 95
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck564 line 97
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource565 line 102
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow565 line 105
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck565 line 107
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck565 line 109
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource566 line 114
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow566 line 117
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck566 line 119
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck566 line 121
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource567 line 126
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow567 line 129
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck567 line 131
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck567 line 133
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource568 line 138
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow568 line 141
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck568 line 143
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck568 line 145
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource569 line 150
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow569 line 153
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck569 line 155
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck569 line 157
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource570 line 161
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow570 line 164
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck570 line 166
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck570 line 168
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource571 line 173
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow571 line 176
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck571 line 178
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck571 line 180
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource572 line 185
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow572 line 188
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck572 line 190
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck572 line 192
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource573 line 197
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow573 line 200
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck573 line 202
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck573 line 204
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource574 line 208
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow574 line 211
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck574 line 213
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck574 line 215
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource575 line 219
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow575 line 222
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck575 line 224
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck575 line 226