OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic8.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource128 line 51
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow128 line 54
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck128 line 56
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck128 line 58
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource129 line 62
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow129 line 65
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck129 line 67
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck129 line 69
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource130 line 74
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow130 line 77
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck130 line 79
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck130 line 81
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource131 line 86
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow131 line 89
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck131 line 91
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck131 line 93
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource132 line 97
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow132 line 100
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck132 line 102
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck132 line 104
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource133 line 108
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow133 line 111
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck133 line 113
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck133 line 115
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource134 line 119
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow134 line 122
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck134 line 124
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck134 line 126
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource135 line 130
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow135 line 133
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck135 line 135
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck135 line 137
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource136 line 141
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow136 line 144
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck136 line 146
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck136 line 148
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource137 line 152
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow137 line 155
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck137 line 157
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck137 line 159
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource138 line 164
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow138 line 167
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck138 line 169
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck138 line 171
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource139 line 176
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow139 line 179
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck139 line 181
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck139 line 183
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource140 line 188
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow140 line 191
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck140 line 193
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck140 line 195
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource141 line 200
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow141 line 203
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck141 line 205
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck141 line 207
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource142 line 212
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow142 line 215
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck142 line 217
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck142 line 219
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource143 line 223
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow143 line 226
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck143 line 228
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck143 line 230