OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic88.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1408 line 35
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1408 line 38
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1408 line 40
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1408 line 42
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1409 line 46
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1409 line 49
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1409 line 51
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1409 line 53
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1410 line 58
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1410 line 61
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1410 line 63
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1410 line 65
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1411 line 70
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1411 line 73
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1411 line 75
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1411 line 77
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1412 line 82
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1412 line 85
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1412 line 87
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1412 line 89
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1413 line 94
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1413 line 97
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1413 line 99
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1413 line 101
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1414 line 106
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1414 line 109
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1414 line 111
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1414 line 113
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1415 line 118
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1415 line 121
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1415 line 123
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1415 line 125
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1416 line 129
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1416 line 132
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1416 line 134
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1416 line 136
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1417 line 140
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1417 line 143
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1417 line 145
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1417 line 147
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1418 line 152
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1418 line 155
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1418 line 157
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1418 line 159
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1419 line 164
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1419 line 167
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1419 line 169
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1419 line 171
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1420 line 176
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1420 line 179
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1420 line 181
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1420 line 183
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1421 line 188
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1421 line 191
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1421 line 193
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1421 line 195
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1422 line 200
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1422 line 203
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1422 line 205
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1422 line 207
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1423 line 212
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1423 line 215
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1423 line 217
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1423 line 219