OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic106.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1696 line 66
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1696 line 69
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1696 line 71
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1696 line 73
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1697 line 77
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1697 line 80
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1697 line 82
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1697 line 84
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1698 line 88
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1698 line 91
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1698 line 93
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1698 line 95
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1699 line 99
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1699 line 102
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1699 line 104
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1699 line 106
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1700 line 110
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1700 line 113
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1700 line 115
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1700 line 117
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1701 line 121
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1701 line 124
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1701 line 126
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1701 line 128
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1702 line 132
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1702 line 135
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1702 line 137
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1702 line 139
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1703 line 144
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1703 line 147
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1703 line 149
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1703 line 151
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1704 line 156
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1704 line 159
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1704 line 161
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1704 line 163
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1705 line 167
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1705 line 170
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1705 line 172
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1705 line 174
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1706 line 178
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1706 line 181
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1706 line 183
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1706 line 185
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1707 line 189
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1707 line 192
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1707 line 194
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1707 line 196
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1708 line 200
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1708 line 203
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1708 line 205
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1708 line 207
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1709 line 212
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1709 line 215
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1709 line 217
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1709 line 219
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1710 line 224
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1710 line 227
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1710 line 229
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1710 line 231
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1711 line 236
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1711 line 239
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1711 line 241
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1711 line 243