OAI/Analysis/MutuallyUnbiased/MixedSources/Rows58.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero928 line 34
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound928 line 127
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero929 line 132
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound929 line 228
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero930 line 233
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound930 line 326
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero931 line 331
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound931 line 421
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero932 line 426
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound932 line 519
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero933 line 524
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound933 line 620
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero934 line 625
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound934 line 679
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero935 line 684
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound935 line 729
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero936 line 734
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound936 line 779
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero937 line 784
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound937 line 814
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero938 line 819
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound938 line 864
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero939 line 869
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound939 line 914
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero940 line 919
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound940 line 952
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero941 line 957
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound941 line 1053
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero942 line 1058
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound942 line 1154
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero943 line 1159
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound943 line 1216
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt928 line 1221
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt929 line 1224
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt930 line 1227
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt931 line 1230
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt932 line 1233
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt933 line 1236
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt934 line 1239
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt935 line 1242
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt936 line 1245
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt937 line 1248
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt938 line 1251
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt939 line 1254
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt940 line 1257
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt941 line 1260
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt942 line 1263
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt943 line 1266
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound58 line 1269