OAI/Analysis/MutuallyUnbiased/MixedSources/Rows35.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero560 line 46
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound560 line 70
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero561 line 75
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound561 line 102
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero562 line 107
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound562 line 131
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero563 line 136
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound563 line 160
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero564 line 165
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound564 line 234
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero565 line 239
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound565 line 308
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero566 line 313
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound566 line 382
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero567 line 387
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound567 line 456
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero568 line 461
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound568 line 530
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero569 line 535
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound569 line 559
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero570 line 564
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound570 line 633
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero571 line 638
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound571 line 707
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero572 line 712
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound572 line 781
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero573 line 786
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound573 line 810
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero574 line 815
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound574 line 839
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero575 line 844
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound575 line 871
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt560 line 876
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt561 line 879
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt562 line 882
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt563 line 885
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt564 line 888
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt565 line 891
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt566 line 894
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt567 line 897
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt568 line 900
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt569 line 903
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt570 line 906
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt571 line 909
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt572 line 912
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt573 line 915
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt574 line 918
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt575 line 921
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound35 line 924