OAI/Analysis/MutuallyUnbiased/MixedSemantics/SingleGroup29.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue473 line 29
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair473 line 31
  3. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue474 line 85
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair474 line 87
  5. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue475 line 141
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair475 line 143
  7. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue476 line 197
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair476 line 199
  9. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue477 line 253
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair477 line 255
  11. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue478 line 309
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair478 line 311
  13. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue479 line 365
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair479 line 367
  15. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue480 line 421
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair480 line 423
  17. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue481 line 477
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair481 line 479
  19. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue482 line 533
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair482 line 535
  21. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue483 line 589
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair483 line 591
  23. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue484 line 645
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair484 line 647
  25. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue485 line 701
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair485 line 703
  27. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue486 line 757
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair486 line 759
  29. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue487 line 813
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair487 line 815
  31. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue488 line 869
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair488 line 871