OAI/Analysis/MutuallyUnbiased/MixedSemantics/SingleGroup15.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue248 line 29
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair248 line 31
  3. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue249 line 95
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair249 line 97
  5. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue250 line 161
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair250 line 163
  7. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue251 line 227
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair251 line 229
  9. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue252 line 293
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair252 line 295
  11. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue253 line 359
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair253 line 361
  13. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue254 line 425
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair254 line 427
  15. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue255 line 491
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair255 line 493
  17. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue256 line 557
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair256 line 559
  19. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue257 line 623
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair257 line 625
  21. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue258 line 689
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair258 line 691
  23. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue259 line 755
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair259 line 757
  25. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue260 line 821
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair260 line 823
  27. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue261 line 887
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair261 line 889
  29. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue262 line 953
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair262 line 955
  31. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue263 line 1019
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair263 line 1021