OAI/Analysis/MutuallyUnbiased/MixedSources/Rows104.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1664 line 66
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1664 line 90
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1665 line 95
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1665 line 122
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1666 line 127
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1666 line 154
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1667 line 159
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1667 line 186
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1668 line 191
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1668 line 284
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1669 line 289
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1669 line 385
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1670 line 390
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1670 line 483
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1671 line 488
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1671 line 512
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1672 line 517
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1672 line 610
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1673 line 615
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1673 line 708
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1674 line 713
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1674 line 806
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1675 line 811
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1675 line 904
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1676 line 909
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1676 line 936
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1677 line 941
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1677 line 965
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1678 line 970
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1678 line 994
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1679 line 999
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1679 line 1086
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1664 line 1091
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1665 line 1094
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1666 line 1097
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1667 line 1100
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1668 line 1103
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1669 line 1106
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1670 line 1109
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1671 line 1112
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1672 line 1115
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1673 line 1118
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1674 line 1121
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1675 line 1124
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1676 line 1127
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1677 line 1130
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1678 line 1133
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1679 line 1136
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound104 line 1139