OAI/Analysis/MutuallyUnbiased/MixedSemantics/SingleGroup31.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue507 line 35
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair507 line 37
  3. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue508 line 91
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair508 line 93
  5. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue509 line 147
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair509 line 149
  7. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue510 line 203
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair510 line 205
  9. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue511 line 259
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair511 line 261
  11. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue512 line 315
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair512 line 317
  13. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue513 line 371
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair513 line 373
  15. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue514 line 427
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair514 line 429
  17. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue515 line 483
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair515 line 485
  19. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue516 line 539
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair516 line 541
  21. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue517 line 595
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair517 line 597
  23. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue518 line 651
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair518 line 653
  25. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue519 line 707
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair519 line 709
  27. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue520 line 763
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair520 line 765
  29. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue521 line 819
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair521 line 821
  31. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue522 line 875
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair522 line 877