OAI/Analysis/MutuallyUnbiased/MixedSemantics/SingleGroup12.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue200 line 30
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair200 line 32
  3. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue201 line 86
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair201 line 88
  5. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue202 line 142
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair202 line 144
  7. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue203 line 198
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair203 line 200
  9. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue204 line 254
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair204 line 256
  11. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue205 line 310
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair205 line 312
  13. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue206 line 366
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair206 line 368
  15. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue207 line 422
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair207 line 424
  17. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue208 line 478
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair208 line 480
  19. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue209 line 534
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair209 line 536
  21. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue210 line 590
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair210 line 592
  23. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue211 line 646
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair211 line 648
  25. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue212 line 702
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair212 line 704
  27. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue213 line 758
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair213 line 760
  29. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue214 line 814
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair214 line 816
  31. def OAI.MUB6.Certificate.MixedSemantics.singlePairValue215 line 870
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singlePair215 line 872