OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic76.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1216 line 29
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1216 line 32
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1216 line 34
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1216 line 36
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1217 line 40
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1217 line 43
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1217 line 45
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1217 line 47
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1218 line 51
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1218 line 54
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1218 line 56
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1218 line 58
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1219 line 62
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1219 line 65
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1219 line 67
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1219 line 69
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1220 line 73
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1220 line 76
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1220 line 78
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1220 line 80
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1221 line 84
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1221 line 87
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1221 line 89
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1221 line 91
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1222 line 95
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1222 line 98
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1222 line 100
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1222 line 102
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1223 line 106
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1223 line 109
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1223 line 111
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1223 line 113
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1224 line 117
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1224 line 120
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1224 line 122
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1224 line 124
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1225 line 128
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1225 line 131
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1225 line 133
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1225 line 135
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1226 line 139
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1226 line 142
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1226 line 144
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1226 line 146
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1227 line 150
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1227 line 153
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1227 line 155
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1227 line 157
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1228 line 162
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1228 line 165
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1228 line 167
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1228 line 169
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1229 line 173
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1229 line 176
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1229 line 178
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1229 line 180
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1230 line 184
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1230 line 187
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1230 line 189
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1230 line 191
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1231 line 195
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1231 line 198
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1231 line 200
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1231 line 202