OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic0.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource0 line 29
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow0 line 32
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck0 line 34
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck0 line 36
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1 line 41
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1 line 44
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1 line 46
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1 line 48
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2 line 53
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2 line 56
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2 line 58
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2 line 60
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource3 line 65
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow3 line 68
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck3 line 70
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck3 line 72
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource4 line 77
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow4 line 80
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck4 line 82
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck4 line 84
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource5 line 89
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow5 line 92
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck5 line 94
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck5 line 96
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource6 line 101
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow6 line 104
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck6 line 106
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck6 line 108
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource7 line 113
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow7 line 116
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck7 line 118
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck7 line 120
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource8 line 125
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow8 line 128
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck8 line 130
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck8 line 132
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource9 line 137
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow9 line 140
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck9 line 142
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck9 line 144
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource10 line 149
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow10 line 152
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck10 line 154
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck10 line 156
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource11 line 161
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow11 line 164
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck11 line 166
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck11 line 168
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource12 line 173
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow12 line 176
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck12 line 178
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck12 line 180
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource13 line 185
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow13 line 188
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck13 line 190
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck13 line 192
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource14 line 197
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow14 line 200
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck14 line 202
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck14 line 204
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource15 line 209
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow15 line 212
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck15 line 214
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck15 line 216