OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic79.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1264 line 40
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1264 line 43
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1264 line 45
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1264 line 47
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1265 line 51
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1265 line 54
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1265 line 56
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1265 line 58
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1266 line 62
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1266 line 65
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1266 line 67
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1266 line 69
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1267 line 73
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1267 line 76
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1267 line 78
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1267 line 80
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1268 line 84
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1268 line 87
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1268 line 89
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1268 line 91
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1269 line 95
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1269 line 98
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1269 line 100
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1269 line 102
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1270 line 106
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1270 line 109
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1270 line 111
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1270 line 113
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1271 line 117
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1271 line 120
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1271 line 122
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1271 line 124
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1272 line 128
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1272 line 131
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1272 line 133
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1272 line 135
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1273 line 139
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1273 line 142
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1273 line 144
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1273 line 146
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1274 line 150
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1274 line 153
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1274 line 155
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1274 line 157
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1275 line 161
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1275 line 164
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1275 line 166
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1275 line 168
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1276 line 172
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1276 line 175
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1276 line 177
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1276 line 179
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1277 line 183
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1277 line 186
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1277 line 188
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1277 line 190
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1278 line 194
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1278 line 197
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1278 line 199
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1278 line 201
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1279 line 205
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1279 line 208
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1279 line 210
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1279 line 212