OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic5.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource80 line 43
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow80 line 46
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck80 line 48
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck80 line 50
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource81 line 54
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow81 line 57
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck81 line 59
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck81 line 61
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource82 line 65
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow82 line 68
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck82 line 70
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck82 line 72
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource83 line 76
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow83 line 79
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck83 line 81
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck83 line 83
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource84 line 87
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow84 line 90
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck84 line 92
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck84 line 94
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource85 line 98
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow85 line 101
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck85 line 103
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck85 line 105
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource86 line 109
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow86 line 112
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck86 line 114
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck86 line 116
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource87 line 120
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow87 line 123
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck87 line 125
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck87 line 127
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource88 line 131
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow88 line 134
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck88 line 136
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck88 line 138
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource89 line 142
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow89 line 145
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck89 line 147
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck89 line 149
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource90 line 153
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow90 line 156
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck90 line 158
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck90 line 160
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource91 line 164
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow91 line 167
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck91 line 169
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck91 line 171
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource92 line 176
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow92 line 179
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck92 line 181
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck92 line 183
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource93 line 188
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow93 line 191
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck93 line 193
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck93 line 195
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource94 line 200
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow94 line 203
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck94 line 205
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck94 line 207
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource95 line 212
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow95 line 215
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck95 line 217
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck95 line 219