OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic129.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2064 line 40
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2064 line 43
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2064 line 45
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2064 line 47
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2065 line 52
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2065 line 55
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2065 line 57
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2065 line 59
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2066 line 63
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2066 line 66
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2066 line 68
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2066 line 70
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2067 line 75
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2067 line 78
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2067 line 80
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2067 line 82
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2068 line 87
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2068 line 90
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2068 line 92
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2068 line 94
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2069 line 98
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2069 line 101
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2069 line 103
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2069 line 105
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2070 line 110
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2070 line 113
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2070 line 115
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2070 line 117
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2071 line 121
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2071 line 124
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2071 line 126
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2071 line 128
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2072 line 133
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2072 line 136
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2072 line 138
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2072 line 140
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2073 line 144
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2073 line 147
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2073 line 149
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2073 line 151
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2074 line 156
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2074 line 159
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2074 line 161
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2074 line 163
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2075 line 167
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2075 line 170
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2075 line 172
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2075 line 174
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2076 line 179
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2076 line 182
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2076 line 184
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2076 line 186
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2077 line 191
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2077 line 194
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2077 line 196
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2077 line 198
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2078 line 203
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2078 line 206
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2078 line 208
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2078 line 210
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2079 line 215
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2079 line 218
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2079 line 220
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2079 line 222