OAI/Analysis/MutuallyUnbiased/MixedSources/Rows60.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero960 line 39
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound960 line 84
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero961 line 89
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound961 line 134
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero962 line 139
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound962 line 184
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero963 line 189
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound963 line 255
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero964 line 260
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound964 line 329
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero965 line 334
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound965 line 424
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero966 line 429
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound966 line 525
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero967 line 530
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound967 line 626
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero968 line 631
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound968 line 694
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero969 line 699
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound969 line 768
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero970 line 773
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound970 line 842
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero971 line 847
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound971 line 916
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero972 line 921
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound972 line 990
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero973 line 995
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound973 line 1064
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero974 line 1069
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound974 line 1150
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero975 line 1155
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound975 line 1248
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt960 line 1253
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt961 line 1256
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt962 line 1259
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt963 line 1262
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt964 line 1265
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt965 line 1268
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt966 line 1271
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt967 line 1274
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt968 line 1277
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt969 line 1280
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt970 line 1283
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt971 line 1286
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt972 line 1289
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt973 line 1292
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt974 line 1295
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt975 line 1298
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound60 line 1301