OAI/Analysis/MutuallyUnbiased/MixedSources/Rows73.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1168 line 54
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1168 line 78
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1169 line 83
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1169 line 152
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1170 line 157
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1170 line 226
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1171 line 231
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1171 line 300
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1172 line 305
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1172 line 329
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1173 line 334
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1173 line 358
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1174 line 363
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1174 line 387
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1175 line 392
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1175 line 416
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1176 line 421
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1176 line 448
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1177 line 453
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1177 line 522
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1178 line 527
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1178 line 596
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1179 line 601
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1179 line 670
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1180 line 675
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1180 line 699
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1181 line 704
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1181 line 728
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1182 line 733
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1182 line 757
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1183 line 762
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1183 line 786
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1168 line 791
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1169 line 794
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1170 line 797
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1171 line 800
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1172 line 803
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1173 line 806
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1174 line 809
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1175 line 812
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1176 line 815
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1177 line 818
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1178 line 821
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1179 line 824
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1180 line 827
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1181 line 830
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1182 line 833
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1183 line 836
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound73 line 839