OAI/Analysis/MutuallyUnbiased/MixedSemantics/SingleGroup3.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue56 line 32
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair56 line 34
  3. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue57 line 88
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair57 line 90
  5. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue58 line 144
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair58 line 146
  7. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue59 line 200
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair59 line 202
  9. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue60 line 256
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair60 line 258
  11. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue61 line 312
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair61 line 314
  13. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue62 line 368
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair62 line 370
  15. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue63 line 424
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair63 line 426
  17. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue64 line 480
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair64 line 482
  19. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue65 line 536
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair65 line 538
  21. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue66 line 592
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair66 line 594
  23. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue67 line 648
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair67 line 650
  25. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue68 line 704
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair68 line 706
  27. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue69 line 760
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair69 line 762
  29. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue70 line 816
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair70 line 818
  31. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue71 line 872
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair71 line 874