OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic84.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1344 line 29
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1344 line 32
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1344 line 34
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1344 line 36
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1345 line 40
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1345 line 43
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1345 line 45
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1345 line 47
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1346 line 51
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1346 line 54
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1346 line 56
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1346 line 58
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1347 line 62
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1347 line 65
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1347 line 67
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1347 line 69
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1348 line 73
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1348 line 76
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1348 line 78
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1348 line 80
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1349 line 84
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1349 line 87
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1349 line 89
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1349 line 91
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1350 line 95
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1350 line 98
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1350 line 100
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1350 line 102
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1351 line 106
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1351 line 109
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1351 line 111
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1351 line 113
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1352 line 117
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1352 line 120
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1352 line 122
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1352 line 124
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1353 line 128
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1353 line 131
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1353 line 133
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1353 line 135
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1354 line 139
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1354 line 142
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1354 line 144
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1354 line 146
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1355 line 150
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1355 line 153
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1355 line 155
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1355 line 157
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1356 line 161
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1356 line 164
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1356 line 166
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1356 line 168
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1357 line 172
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1357 line 175
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1357 line 177
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1357 line 179
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1358 line 183
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1358 line 186
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1358 line 188
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1358 line 190
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1359 line 194
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1359 line 197
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1359 line 199
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1359 line 201