OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic104.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1664 line 66
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1664 line 69
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1664 line 71
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1664 line 73
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1665 line 77
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1665 line 80
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1665 line 82
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1665 line 84
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1666 line 88
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1666 line 91
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1666 line 93
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1666 line 95
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1667 line 99
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1667 line 102
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1667 line 104
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1667 line 106
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1668 line 110
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1668 line 113
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1668 line 115
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1668 line 117
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1669 line 122
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1669 line 125
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1669 line 127
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1669 line 129
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1670 line 134
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1670 line 137
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1670 line 139
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1670 line 141
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1671 line 145
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1671 line 148
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1671 line 150
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1671 line 152
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1672 line 156
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1672 line 159
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1672 line 161
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1672 line 163
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1673 line 168
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1673 line 171
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1673 line 173
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1673 line 175
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1674 line 180
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1674 line 183
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1674 line 185
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1674 line 187
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1675 line 192
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1675 line 195
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1675 line 197
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1675 line 199
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1676 line 203
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1676 line 206
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1676 line 208
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1676 line 210
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1677 line 214
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1677 line 217
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1677 line 219
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1677 line 221
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1678 line 225
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1678 line 228
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1678 line 230
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1678 line 232
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1679 line 236
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1679 line 239
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1679 line 241
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1679 line 243