OAI/Analysis/MutuallyUnbiased/MixedSemantics/SingleGroup16.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue264 line 36
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair264 line 38
  3. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue265 line 92
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair265 line 94
  5. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue266 line 148
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair266 line 150
  7. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue267 line 204
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair267 line 206
  9. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue268 line 260
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair268 line 262
  11. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue269 line 316
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair269 line 318
  13. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue270 line 372
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair270 line 374
  15. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue271 line 428
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair271 line 430
  17. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue272 line 484
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair272 line 486
  19. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue273 line 540
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair273 line 542
  21. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue274 line 596
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair274 line 598
  23. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue275 line 652
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair275 line 654
  25. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue276 line 708
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair276 line 710
  27. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue277 line 764
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair277 line 766
  29. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue278 line 820
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair278 line 822
  31. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue279 line 876
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair279 line 878