OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic91.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1456 line 39
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1456 line 42
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1456 line 44
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1456 line 46
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1457 line 50
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1457 line 53
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1457 line 55
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1457 line 57
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1458 line 61
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1458 line 64
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1458 line 66
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1458 line 68
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1459 line 72
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1459 line 75
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1459 line 77
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1459 line 79
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1460 line 83
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1460 line 86
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1460 line 88
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1460 line 90
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1461 line 94
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1461 line 97
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1461 line 99
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1461 line 101
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1462 line 105
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1462 line 108
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1462 line 110
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1462 line 112
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1463 line 116
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1463 line 119
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1463 line 121
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1463 line 123
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1464 line 127
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1464 line 130
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1464 line 132
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1464 line 134
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1465 line 138
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1465 line 141
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1465 line 143
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1465 line 145
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1466 line 149
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1466 line 152
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1466 line 154
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1466 line 156
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1467 line 160
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1467 line 163
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1467 line 165
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1467 line 167
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1468 line 171
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1468 line 174
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1468 line 176
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1468 line 178
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1469 line 182
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1469 line 185
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1469 line 187
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1469 line 189
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1470 line 193
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1470 line 196
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1470 line 198
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1470 line 200
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1471 line 204
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1471 line 207
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1471 line 209
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1471 line 211