OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic2.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource32 line 27
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow32 line 30
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck32 line 32
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck32 line 34
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource33 line 38
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow33 line 41
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck33 line 43
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck33 line 45
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource34 line 49
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow34 line 52
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck34 line 54
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck34 line 56
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource35 line 60
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow35 line 63
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck35 line 65
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck35 line 67
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource36 line 72
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow36 line 75
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck36 line 77
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck36 line 79
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource37 line 83
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow37 line 86
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck37 line 88
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck37 line 90
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource38 line 94
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow38 line 97
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck38 line 99
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck38 line 101
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource39 line 105
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow39 line 108
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck39 line 110
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck39 line 112
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource40 line 116
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow40 line 119
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck40 line 121
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck40 line 123
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource41 line 127
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow41 line 130
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck41 line 132
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck41 line 134
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource42 line 138
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow42 line 141
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck42 line 143
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck42 line 145
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource43 line 149
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow43 line 152
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck43 line 154
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck43 line 156
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource44 line 160
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow44 line 163
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck44 line 165
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck44 line 167
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource45 line 171
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow45 line 174
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck45 line 176
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck45 line 178
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource46 line 182
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow46 line 185
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck46 line 187
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck46 line 189
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource47 line 193
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow47 line 196
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck47 line 198
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck47 line 200