OAI/Analysis/MutuallyUnbiased/MixedSemantics/SingleGroup30.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue489 line 31
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair489 line 33
  3. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue490 line 87
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair490 line 89
  5. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue491 line 143
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair491 line 145
  7. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue492 line 199
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair492 line 201
  9. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue493 line 255
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair493 line 257
  11. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue494 line 311
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair494 line 313
  13. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue495 line 367
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair495 line 369
  15. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue497 line 423
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair497 line 425
  17. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue498 line 479
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair498 line 481
  19. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue499 line 535
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair499 line 537
  21. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue500 line 591
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair500 line 593
  23. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue501 line 647
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair501 line 649
  25. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue502 line 703
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair502 line 705
  27. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue503 line 759
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair503 line 761
  29. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue504 line 815
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair504 line 817
  31. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue506 line 871
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair506 line 873