OAI/Analysis/MutuallyUnbiased/MixedSources/Rows125.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2000 line 49
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2000 line 142
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2001 line 147
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2001 line 174
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2002 line 179
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2002 line 266
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2003 line 271
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2003 line 364
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2004 line 369
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2004 line 435
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2005 line 440
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2005 line 533
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2006 line 538
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2006 line 604
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2007 line 609
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2007 line 675
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2008 line 680
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2008 line 704
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2009 line 709
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2009 line 730
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2010 line 735
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2010 line 804
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2011 line 809
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2011 line 875
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2012 line 880
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2012 line 943
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2013 line 948
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2013 line 969
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2014 line 974
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2014 line 1022
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2015 line 1027
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2015 line 1075
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2000 line 1080
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2001 line 1083
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2002 line 1086
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2003 line 1089
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2004 line 1092
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2005 line 1095
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2006 line 1098
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2007 line 1101
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2008 line 1104
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2009 line 1107
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2010 line 1110
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2011 line 1113
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2012 line 1116
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2013 line 1119
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2014 line 1122
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2015 line 1125
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound125 line 1128