OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic100.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1600 line 29
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1600 line 32
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1600 line 34
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1600 line 36
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1601 line 40
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1601 line 43
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1601 line 45
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1601 line 47
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1602 line 51
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1602 line 54
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1602 line 56
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1602 line 58
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1603 line 62
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1603 line 65
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1603 line 67
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1603 line 69
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1604 line 73
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1604 line 76
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1604 line 78
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1604 line 80
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1605 line 84
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1605 line 87
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1605 line 89
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1605 line 91
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1606 line 95
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1606 line 98
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1606 line 100
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1606 line 102
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1607 line 106
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1607 line 109
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1607 line 111
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1607 line 113
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1608 line 117
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1608 line 120
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1608 line 122
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1608 line 124
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1609 line 128
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1609 line 131
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1609 line 133
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1609 line 135
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1610 line 139
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1610 line 142
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1610 line 144
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1610 line 146
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1611 line 150
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1611 line 153
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1611 line 155
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1611 line 157
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1612 line 161
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1612 line 164
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1612 line 166
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1612 line 168
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1613 line 172
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1613 line 175
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1613 line 177
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1613 line 179
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1614 line 183
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1614 line 186
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1614 line 188
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1614 line 190
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1615 line 194
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1615 line 197
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1615 line 199
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1615 line 201