OAI/Analysis/MutuallyUnbiased/MixedSources/Rows135.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2160 line 20
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2160 line 44
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2161 line 49
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2161 line 76
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2162 line 81
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2162 line 108
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2163 line 113
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2163 line 137
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2164 line 142
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2164 line 166
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2165 line 171
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2165 line 186
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2166 line 191
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2167 line 197
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2168 line 203
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2169 line 209
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2170 line 215
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2171 line 221
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2172 line 227
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2173 line 233
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2174 line 239
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2175 line 245
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2160 line 251
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2161 line 254
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2162 line 257
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2163 line 260
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2164 line 263
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2165 line 266
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2166 line 269
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2167 line 272
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2168 line 275
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2169 line 278
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2170 line 281
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2171 line 284
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2172 line 287
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2173 line 290
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2174 line 293
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2175 line 296
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound135 line 299