OAI/Analysis/MutuallyUnbiased/MixedSources/Rows121.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1936 line 52
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1936 line 121
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1937 line 126
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1937 line 222
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1938 line 227
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1938 line 323
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1939 line 328
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1939 line 352
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1940 line 357
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1940 line 381
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1941 line 386
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1941 line 482
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1942 line 487
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1942 line 583
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1943 line 588
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1943 line 615
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1944 line 620
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1944 line 713
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1945 line 718
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1945 line 787
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1946 line 792
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1946 line 861
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1947 line 866
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1947 line 890
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1948 line 895
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1948 line 964
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1949 line 969
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1949 line 1065
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1950 line 1070
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1950 line 1166
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1951 line 1171
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1951 line 1198
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1936 line 1203
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1937 line 1206
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1938 line 1209
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1939 line 1212
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1940 line 1215
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1941 line 1218
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1942 line 1221
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1943 line 1224
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1944 line 1227
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1945 line 1230
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1946 line 1233
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1947 line 1236
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1948 line 1239
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1949 line 1242
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1950 line 1245
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1951 line 1248
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound121 line 1251