OAI/Analysis/MutuallyUnbiased/MixedSemantics/SingleGroup9.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue152 line 29
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair152 line 31
  3. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue153 line 95
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair153 line 97
  5. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue154 line 161
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair154 line 163
  7. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue155 line 227
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair155 line 229
  9. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue156 line 293
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair156 line 295
  11. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue157 line 359
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair157 line 361
  13. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue158 line 425
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair158 line 427
  15. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue159 line 491
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair159 line 493
  17. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue160 line 557
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair160 line 559
  19. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue161 line 623
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair161 line 625
  21. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue162 line 689
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair162 line 691
  23. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue163 line 755
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair163 line 757
  25. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue164 line 821
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair164 line 823
  27. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue165 line 887
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair165 line 889
  29. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue166 line 953
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair166 line 955
  31. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue167 line 1019
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair167 line 1021