OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic98.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1568 line 47
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1568 line 50
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1568 line 52
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1568 line 54
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1569 line 59
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1569 line 62
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1569 line 64
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1569 line 66
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1570 line 71
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1570 line 74
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1570 line 76
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1570 line 78
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1571 line 82
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1571 line 85
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1571 line 87
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1571 line 89
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1572 line 94
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1572 line 97
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1572 line 99
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1572 line 101
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1573 line 106
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1573 line 109
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1573 line 111
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1573 line 113
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1574 line 117
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1574 line 120
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1574 line 122
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1574 line 124
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1575 line 128
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1575 line 131
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1575 line 133
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1575 line 135
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1576 line 140
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1576 line 143
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1576 line 145
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1576 line 147
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1577 line 152
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1577 line 155
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1577 line 157
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1577 line 159
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1578 line 163
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1578 line 166
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1578 line 168
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1578 line 170
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1579 line 174
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1579 line 177
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1579 line 179
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1579 line 181
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1580 line 185
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1580 line 188
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1580 line 190
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1580 line 192
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1581 line 196
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1581 line 199
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1581 line 201
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1581 line 203
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1582 line 207
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1582 line 210
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1582 line 212
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1582 line 214
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1583 line 218
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1583 line 221
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1583 line 223
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1583 line 225