OAI/Analysis/MutuallyUnbiased/MixedSemantics/SingleGroup5.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue88 line 26
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair88 line 28
  3. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue89 line 82
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair89 line 84
  5. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue90 line 138
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair90 line 140
  7. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue91 line 194
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair91 line 196
  9. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue92 line 250
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair92 line 252
  11. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue93 line 306
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair93 line 308
  13. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue94 line 362
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair94 line 364
  15. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue95 line 418
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair95 line 420
  17. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue96 line 474
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair96 line 476
  19. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue97 line 530
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair97 line 532
  21. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue98 line 586
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair98 line 588
  23. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue99 line 642
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair99 line 644
  25. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue100 line 698
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair100 line 700
  27. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue101 line 754
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair101 line 756
  29. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue102 line 810
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair102 line 812
  31. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue103 line 866
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair103 line 868