OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic70.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1120 line 57
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1120 line 60
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1120 line 62
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1120 line 64
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1121 line 69
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1121 line 72
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1121 line 74
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1121 line 76
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1122 line 81
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1122 line 84
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1122 line 86
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1122 line 88
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1123 line 92
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1123 line 95
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1123 line 97
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1123 line 99
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1124 line 104
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1124 line 107
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1124 line 109
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1124 line 111
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1125 line 116
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1125 line 119
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1125 line 121
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1125 line 123
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1126 line 127
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1126 line 130
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1126 line 132
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1126 line 134
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1127 line 138
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1127 line 141
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1127 line 143
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1127 line 145
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1128 line 149
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1128 line 152
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1128 line 154
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1128 line 156
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1129 line 160
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1129 line 163
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1129 line 165
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1129 line 167
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1130 line 171
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1130 line 174
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1130 line 176
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1130 line 178
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1131 line 183
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1131 line 186
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1131 line 188
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1131 line 190
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1132 line 195
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1132 line 198
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1132 line 200
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1132 line 202
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1133 line 206
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1133 line 209
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1133 line 211
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1133 line 213
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1134 line 217
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1134 line 220
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1134 line 222
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1134 line 224
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1135 line 228
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1135 line 231
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1135 line 233
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1135 line 235