OAI/Analysis/MutuallyUnbiased/MixedSemantics/SingleGroup2.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue40 line 32
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair40 line 34
  3. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue41 line 88
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair41 line 90
  5. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue42 line 144
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair42 line 146
  7. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue43 line 200
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair43 line 202
  9. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue44 line 256
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair44 line 258
  11. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue45 line 312
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair45 line 314
  13. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue46 line 368
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair46 line 370
  15. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue47 line 424
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair47 line 426
  17. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue48 line 480
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair48 line 482
  19. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue49 line 536
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair49 line 538
  21. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue50 line 592
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair50 line 594
  23. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue51 line 648
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair51 line 650
  25. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue52 line 704
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair52 line 706
  27. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue53 line 760
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair53 line 762
  29. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue54 line 816
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair54 line 818
  31. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue55 line 872
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair55 line 874