OAI/Analysis/MutuallyUnbiased/MixedSources/Rows54.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero864 line 47
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound864 line 116
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero865 line 121
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound865 line 190
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero866 line 195
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound866 line 264
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero867 line 269
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound867 line 338
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero868 line 343
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound868 line 439
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero869 line 444
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound869 line 471
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero870 line 476
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound870 line 503
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero871 line 508
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound871 line 598
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero872 line 603
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound872 line 699
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero873 line 704
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound873 line 800
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero874 line 805
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound874 line 832
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero875 line 837
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound875 line 864
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero876 line 869
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound876 line 896
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero877 line 901
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound877 line 997
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero878 line 1002
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound878 line 1098
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero879 line 1103
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound879 line 1130
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt864 line 1135
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt865 line 1138
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt866 line 1141
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt867 line 1144
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt868 line 1147
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt869 line 1150
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt870 line 1153
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt871 line 1156
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt872 line 1159
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt873 line 1162
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt874 line 1165
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt875 line 1168
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt876 line 1171
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt877 line 1174
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt878 line 1177
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt879 line 1180
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound54 line 1183