OAI/Analysis/MutuallyUnbiased/MixedSources/Rows124.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1984 line 52
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1984 line 145
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1985 line 150
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1985 line 243
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1986 line 248
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1986 line 341
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1987 line 346
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1987 line 373
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1988 line 378
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1988 line 468
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1989 line 473
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1989 line 569
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1990 line 574
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1990 line 643
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1991 line 648
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1991 line 717
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1992 line 722
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1992 line 791
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1993 line 796
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1993 line 859
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1994 line 864
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1994 line 933
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1995 line 938
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1995 line 1034
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1996 line 1039
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1996 line 1135
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1997 line 1140
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1997 line 1167
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1998 line 1172
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1998 line 1268
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1999 line 1273
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1999 line 1366
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1984 line 1371
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1985 line 1374
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1986 line 1377
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1987 line 1380
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1988 line 1383
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1989 line 1386
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1990 line 1389
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1991 line 1392
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1992 line 1395
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1993 line 1398
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1994 line 1401
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1995 line 1404
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1996 line 1407
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1997 line 1410
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1998 line 1413
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1999 line 1416
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound124 line 1419