OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic99.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1584 line 40
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1584 line 43
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1584 line 45
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1584 line 47
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1585 line 52
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1585 line 55
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1585 line 57
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1585 line 59
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1586 line 63
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1586 line 66
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1586 line 68
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1586 line 70
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1587 line 74
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1587 line 77
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1587 line 79
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1587 line 81
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1588 line 86
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1588 line 89
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1588 line 91
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1588 line 93
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1589 line 98
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1589 line 101
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1589 line 103
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1589 line 105
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1590 line 110
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1590 line 113
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1590 line 115
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1590 line 117
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1591 line 121
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1591 line 124
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1591 line 126
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1591 line 128
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1592 line 132
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1592 line 135
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1592 line 137
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1592 line 139
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1593 line 143
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1593 line 146
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1593 line 148
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1593 line 150
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1594 line 155
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1594 line 158
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1594 line 160
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1594 line 162
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1595 line 166
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1595 line 169
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1595 line 171
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1595 line 173
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1596 line 178
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1596 line 181
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1596 line 183
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1596 line 185
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1597 line 189
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1597 line 192
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1597 line 194
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1597 line 196
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1598 line 200
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1598 line 203
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1598 line 205
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1598 line 207
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1599 line 212
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1599 line 215
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1599 line 217
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1599 line 219